Library hilbert.diag
Require Import Ensembles.
Require Import Epsilon.
Require Import Classical.
Section phi.
Variable phi : nat -> Ensemble nat.
Hypothesis phi_surs : forall E, exists n, phi n = E.
Let E' : Ensemble nat := fun p => ~ (In _ (phi p) p).
Let p := epsilon 0 (fun p => phi p = E').
Remark R1 : In _ E' p -> In _ (phi p) p.
pattern p.
hilbert_e.
unfold E'.
unfold In.
intro.
intros. rewrite H.
auto.
Qed.
Remark R2: In _ E' p -> ~ In _ (phi p) p.
pattern p; hilbert_e.
Qed.
Remark R3 : ~ In _ E' p -> ~ In _ (phi p) p.
pattern p; hilbert_e.
intros.
rewrite <- H in H0.
auto.
Qed.
Remark R4 : ~ In _ E' p -> In _ (phi p) p.
pattern p; hilbert_e.
intros.
rewrite H.
red.
unfold E' in H0.
unfold In in H0.
rewrite <-H.
apply NNPP.
auto.
Qed.
Lemma paradox : False.
case (classic (In _ E' p)).
intro H.
case (R2 H).
apply R1;auto.
intro H.
case (R3 H).
apply R4;auto.
Qed.
End phi.
Check paradox.