Mercurial > cpdt > repo

comparison src/Equality.v @ 271:aa3c054afce0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some bug fixes while working on JFR version
author Adam Chlipala <adamc@hcoop.net>
date Mon, 19 Apr 2010 16:49:26 -0400
parents c8508d277a00
children 19fbda8a8117
comparison
equal deleted inserted replaced
270:fd46d077b952 271:aa3c054afce0
572 end. 572 end.
573 (* end thide *) 573 (* end thide *)
574 574
575 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial. 575 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
576 576
577 Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *) 577 Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *)
578 578
579 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x), 579 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
580 O = match pf with refl_equal => O end. 580 O = match pf with refl_equal => O end.
581 (* begin thide *) 581 (* begin thide *)
582 intros; rewrite (UIP_refl' pf); reflexivity. 582 intros; rewrite (UIP_refl' pf); reflexivity.