import Sol;

Inductive [V : El Prop]
Relation_LE
Constructors [VI : (Z : (A : El Prop)(R : (P : (x : El (Prf A)) El Prop) (x : El (Prf A)) El Prop) (a : El (Prf A)) El Prop) Prf V];

Claim Vapp : (Z : Prf V)(A : Prop)((Prf A -> Prop) -> Prf A -> Prop) -> Prf A -> Prop;
Intros Z A R a; Refine E_V; Refine Z; Intros F; Refine F; Refine a; Refine R; ReturnAll;

Inductive [U : El Prop]
Relation_LE
Constructors [UI : (F : (Z : El (Prf V)) El Prop) Prf U];

Claim Uapp : (F : Prf U)Prf V -> Prop;
Intros F Z; Refine E_U; Refine F; Intros FF; Refine FF; Refine Z; ReturnAll;

Claim sb : (A : Prop)((Prf A -> Prop) -> Prf A -> Prop) -> Prf A -> Prf U;
Intros A R a; Refine UI; Intros Z; Refine R; Refine a;
Refine (Vapp Z A R); ReturnAll;

(* [sb [A : Prop][R : (Prf A -> Prop) -> Prf A -> Prop][a : Prf A] = UI ([Z : Prf V] R (Vapp Z A R) a) : Prf U] *)

Claim le : (Prf U -> Prop) -> Prf U -> Prop;
Intros i x; Refine Uapp; 2 Refine x;
Refine VI; Intros A R a; Refine i; Refine sb; Refine a; Refine R; ReturnAll;

(* [le [i : Prf U -> Prop][x : Prf U] =
Uapp x (VI [A : Prop][R : (Prf A -> Prop) -> Prf A -> Prop][a : Prf A]
i (sb A R a))] *)

Inductive [i : (u : El (Prf U)) El Prop] [induct : El Prop]
Relation
Constructors [inductI : (H : (x : El (Prf U))(K : El (Prf (le i x)))
El (Prf (i x))) Prf induct];

Claim induct_app : (i : Prf U -> Prop)Prf (induct i) -> (x : Prf U)
 (Prf (le i x)) -> Prf (i x);
Intros i H x K; Refine E_induct; Refine H; Intros F; Refine F;
Refine K; ReturnAll;

Claim WF : Prf U; Refine UI; Intros z; Refine induct;
Refine Vapp; Refine le; Refine z; ReturnAll;

(* [WF = UI [z:Prf V] induct (Vapp z U le) : Prf U] *)

[B : Prop];
Inductive [x : El (Prf U)] [I : El Prop]
Relation
Constructors [II : (F : (H : (i : (x : El (Prf U)) El Prop) (K : El (Prf (le i x))) El (Prf (i (sb U le x)))) El (Prf B)) Prf I];

Claim Iapp : (x : Prf U) Prf (I x) ->
((i : Prf U -> Prop) Prf (le i x) -> Prf (i (sb U le x))) -> Prf B;
Intros x H F; Refine E_I; Refine H; Intros G; Refine G; Refine F; ReturnAll;

Claim omega : (i : Prf U -> Prop)Prf (induct i) -> Prf (i WF);
Intros i y; Refine induct_app i; 2 Refine y; Expand le; Expand WF; Expand
Uapp; NormalType m_3; Expand Vapp; NormalType m_3;
Refine inductI; Intros x; Refine induct_app i y (sb U le x); ReturnAll;

Claim lemma : Prf (induct I);
Refine inductI; Intros x p; Refine II; Intros q;
Refine Iapp; 2 Refine q I; 2 Refine p; Intros i;
Refine q; ReturnAll;

Claim lemma2 : ((i : Prf U -> Prop)Prf (induct i) -> Prf (i WF)) -> Prf B;
Intros x;
Refine Iapp; 2 Refine x I; 2 Refine lemma;
Intros i; Refine x; ReturnAll;

Claim paradox : Prf B;
Refine lemma2 omega;