diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-18 20:39:34 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-24 12:25:55 +0200 |
| commit | e8e994afb5a29f92c750fb370d01b704ddf06cc4 (patch) | |
| tree | b971d0e9083c049c5fd0058bf316c4972589744a /theories/Logic/ClassicalFacts.v | |
| parent | 2739fe8a22a9df48e717583d6efabc42e41f9814 (diff) | |
A new version of Hurkens.v.
Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.
Diffstat (limited to 'theories/Logic/ClassicalFacts.v')
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 34ae1cd5b..1a70f7806 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -367,7 +367,7 @@ Section Proof_irrelevance_EM_CC. Proof. refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H. trivial. - apply (paradox B p2b b2p (p2p2 H) p2p1). + apply (NoRetractFromSmallPropositionToProp.paradox B p2b b2p (p2p2 H) p2p1). Qed. End Proof_irrelevance_EM_CC. |