Require Import Bool.
Section G.
Hypothesis cl:(A : Prop)  {A}+{~ A}.
 
Definition P2b : Prop ->  bool :=
   [A : Prop]  Cases (cl A) of (left _) => true | (right _) => false end.
 
Definition b2P : bool ->  Prop :=
   [b : bool]  Cases b of true => True | fase => False end.
 
Lemma p2p: (A : Prop)  (iff (b2P (P2b A)) A).
Intros A; Split.
Unfold P2b b2P.
Elim (cl A).
Auto.
Intros; Contradiction.
Unfold b2P P2b.
Intro; Elim (cl A); Auto.
Qed.
Syntactic Definition p2p_1 := <?, ?> Fst {(p2p ?)}.
 
Definition retract : (A : Prop) A ->  (b2P (P2b A)) :=
   [A : Prop]  <?, ?> Snd {(p2p A)}.
 
Definition V : Set := (A : Set) ((A ->  bool) -> A ->  bool) -> A ->  bool.
 
Definition U : Set := V ->  bool.
 
Definition sb : (A : Set) ((A ->  bool) -> A ->  bool) -> A -> V ->  bool :=
   [A : Set] [r : (A ->  bool) -> A ->  bool] [a : A] [z : V]  (r (z ? r) a).
Syntactic Definition Sb := (sb ?).
 
Definition le : (U ->  bool) -> U ->  bool :=
   [i : U ->  bool]
   [x : U]  (x [A : Set] [r : (A ->  bool) -> A ->  bool] [a : A]  (i (Sb r a))).
 
Definition induct : (U ->  bool) ->  bool :=
   [i : U ->  bool]  (P2b (x : U) (b2P (le i x)) ->  (b2P (i x))).
 
Definition WF : V ->  bool := [z : V]  (induct (z ? le)).
 
Definition Ibis : U ->  bool :=
   [x : U]
    (P2b ((i : U ->  bool) (b2P (le i x)) ->  (b2P (i (Sb le x)))) ->  False).
 
Lemma omega: (i : U ->  bool) (b2P (induct i)) ->  (b2P (i WF)).
Intros i y.
Unfold induct in y.
Generalize (p2p_1 y).
Intros.
Apply H.
Unfold le WF induct.
Apply retract.
Intros x H0.
Apply H.
Exact H0.
Qed.
 
Lemma lemma: (b2P (induct Ibis)).
Unfold induct.
Apply retract.
Intros x p.
Unfold Ibis.
Apply retract.
Intros q.
Generalize (q Ibis p).
Intros H.
Unfold Ibis in H.
Generalize (p2p_1 H).
Intros H0.
Apply H0.
Intros i; Exact (q [y : U]  (i (Sb le y))).
Qed.
 
Lemma lemma2: ((i : U ->  bool) (b2P (induct i)) ->  (b2P (i WF))) ->  False.
Intros x.
Generalize (x Ibis lemma).
Intros H.
Unfold Ibis WF in H.
Generalize (p2p_1 H).
Intros H1.
Apply H1.
Intros i.
Generalize (x [y : U]  (i (Sb le y))).
Intros H0 H3.
Apply H0.
Exact H3.
Qed.
 
Lemma par: False.
Exact (lemma2 omega).
Qed.
End G.