Mercurial > cpdt > repo

comparison src/Universes.v @ 353:3322367e955d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Move GeneralRec one chapter slot later, since Subset should be a prereq
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Oct 2011 17:14:28 -0400
parents ad315efc3b6b
children 252ba054a1cd
comparison
equal deleted inserted replaced
352:ab60b10890ed 353:3322367e955d
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 7. *) 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. *)
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.