summaryrefslogtreecommitdiff
path: root/theories/Logic/Berardi.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Logic/Berardi.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Logic/Berardi.v')
-rw-r--r--theories/Logic/Berardi.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 9eaef07a..5b2f5063 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Berardi.v 8122 2006-03-04 19:26:40Z herbelin $ i*)
+(*i $Id$ i*)
(** This file formalizes Berardi's paradox which says that in
the calculus of constructions, excluded middle (EM) and axiom of
@@ -67,10 +67,10 @@ Section Retracts.
Variables A B : Prop.
-Record retract : Prop :=
+Record retract : Prop :=
{i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
-Record retract_cond : Prop :=
+Record retract_cond : Prop :=
{i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.
@@ -94,7 +94,7 @@ Proof.
intros A B.
destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf].
exists f0 g0; trivial.
- exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
+ exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
destruct hf; auto.
Qed.