Mercurial > cpdt > repo

comparison src/Universes.v @ 350:ad315efc3b6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.