Library HurkensElimRestr

Inductive Prp : Prop :=
prp : Prop -> Prp.

Axiom matchPrp : forall X:Type, (Prop -> X) -> Prp -> X.
Axiom matchPrpeq : forall X:Type, forall f:(Prop -> X), forall A:Prop, matchPrp X f (prp A) = f A.

Definition prop : Prp -> Prop := matchPrp Prop (fun A => A).
Lemma prop_prp : forall A:Prop, prop (prp A) = A.
intros A. unfold prop. apply matchPrpeq.
Qed.

Lemma Hurkens : False.
Proof.
pose (P (X:Prop) := X -> Prp).
pose (U := forall X:Prop, (P (P X) -> X) -> P (P X)).
pose (tau (t : P (P U)) X f p := t (fun x => p (f (x X f)))).
pose (sigma (s : U) := s U tau).
pose (Delta y := prp ((forall p : P U, prop (sigma y p) -> prop (p (tau (sigma y)))) -> False)).
pose (Omega := tau (fun p => prp (forall x : U, prop (sigma x p) -> prop (p x)))).
assert (L : forall p : P U, (forall x : U, prop (sigma x p) -> prop (p x)) -> prop (p Omega)).
  intros p H. apply H.
  unfold sigma. unfold Omega. unfold tau at 1. rewrite prop_prp.
  intros x. exact (H (tau (sigma x))).
cut (forall p : P U, prop (sigma Omega p) -> prop (p (tau (sigma Omega)))).
  generalize (L Delta). unfold Delta at 3. rewrite prop_prp.
  intros H1. apply H1.
  intros x H2. unfold Delta. rewrite prop_prp. intros H3.
  generalize (H3 Delta H2).
  unfold Delta. rewrite prop_prp.
  intros H4. apply H4.
  intros p. apply (H3 (fun y => p (tau (sigma y)))).
intros p. unfold sigma at 1. unfold Omega at 1. unfold tau at 1.
rewrite prop_prp.
apply (L (fun y => p (tau (sigma y)))).
Show Proof.
Defined.