From c2e495922a4c437eb5b486a20eb2040bbf313bf5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 3 Jun 2018 19:39:25 +0200 Subject: 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. --- theories/Logic/Berardi.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'theories') 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. -- cgit v1.2.3