Mercurial > cpdt > repo
comparison src/Universes.v @ 350:ad315efc3b6b
Stub out new chapter
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 26 Oct 2011 11:19:52 -0400 |
parents | 518c8994a715 |
children | 3322367e955d |
comparison
equal
deleted
inserted
replaced
349:de7db21a016c | 350:ad315efc3b6b |
---|---|
610 Print proof_irrelevance. | 610 Print proof_irrelevance. |
611 (** %\vspace{-.15in}% [[ | 611 (** %\vspace{-.15in}% [[ |
612 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ] | 612 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ] |
613 ]] | 613 ]] |
614 | 614 |
615 This axiom asserts that any two proofs of the same proposition are equal. If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable. However, equality is a stronger notion than logical equivalence. Recall this example function from Chapter 6. *) | 615 This axiom asserts that any two proofs of the same proposition are equal. If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable. However, equality is a stronger notion than logical equivalence. Recall this example function from Chapter 7. *) |
616 | 616 |
617 (* begin hide *) | 617 (* begin hide *) |
618 Lemma zgtz : 0 > 0 -> False. | 618 Lemma zgtz : 0 > 0 -> False. |
619 crush. | 619 crush. |
620 Qed. | 620 Qed. |