diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-03 19:39:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-03 20:25:02 +0200 |
| commit | c2e495922a4c437eb5b486a20eb2040bbf313bf5 (patch) | |
| tree | 1a4784ea4eb8b70e23876787649b53055b397acf /theories | |
| parent | c2279eea0b8666282e640637a74947ba554627d6 (diff) | |
Fixing typos in file Berardi.v
Note that one of them is in the name of the main theorem, so we use a
compatibility notation.
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. |