diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-05 13:27:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-05 13:27:44 +0200 |
| commit | c7f8af076b3f9bcfd4ff84ca9a14fc65ab9b953d (patch) | |
| tree | 25f35644737c849d4690570c3d23b36d1f5af222 /theories | |
| parent | b34725f980291daf4fc4d4c589320d4b69f4e2d4 (diff) | |
| parent | c2e495922a4c437eb5b486a20eb2040bbf313bf5 (diff) | |
Merge PR #7690: Fixing typos in file Berardi.v
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/Berardi.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index c6836a1c7..ed4d69ab0 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -82,7 +82,7 @@ End Retracts. (** This lemma is basically a commutation of implication and existential quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) which is provable in classical logic ( => is already provable in - intuitionnistic logic). *) + intuitionistic logic). *) Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). Proof. @@ -136,7 +136,7 @@ trivial. Qed. -Theorem classical_proof_irrelevence : T = F. +Theorem classical_proof_irrelevance : T = F. Proof. generalize not_has_fixpoint. unfold Not_b. @@ -148,4 +148,7 @@ intros not_true is_true. elim not_true; trivial. Qed. + +Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8"). + End Berardis_paradox. |