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.