Mercurial > cpdt > repo
comparison src/Equality.v @ 271:aa3c054afce0
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. |