(******************************************************************************)
(*                      Zermelo Set Theory + atomic sets                      *)
(*                                                                            *)
(*                           Claudio Sacerdoti Coen                           *)
(*                                                                            *)
(*    Based on                                                                *)
(*                                                                            *)
(*                            Zermolo Set Theory                              *)
(*                                                                            *)
(*                              Benjamin Werner                               *)
(*                                                                            *)
(******************************************************************************)

(* This is an extension of Benjamin's encoding of usual Set Theory where I    *)
(* assume the existence of exactly one atomic set for each object t of type T *)
(* where T is a Type in Coq: if (t:T) and (T:Type) then ((atom T t):Ens)      *)
(* The usual axioms of set theory are modified so that they work in the       *)
(* usual way if applied to "normal" sets, and in a reasonable way when        *)
(* applied to atomic sets (for example (Union (atom T t) E) is equal to E for *)
(* each non-atomic set E)                                                     *)
(* All this has been already studied by Fraenkel and Mostowski in the '40,    *)
(* but with totally different goals (in order to proove some independence     *)
(* results in set theory)                                                     *)

(* This is the introduction to the original encoding of Benjamin:             *)
(*    This is an encoding of usual Set Theory, simillar to Peter Aczel's work *)
(*    in the early 80's. The main difference is that the propositions here    *)
(*    live in the impredicative world of "Prop". Thus, priority is given to   *)
(*    expressivity against constructivity.                                    *)
(*                                                                            *)
(*    Since the definition of Sets is the same for both approaches, I added   *)
(*    most  of Aczel's encoding of CZF at the end of the file. Many           *)
(*    definitions are common to both aproaches.                               *)

(* In this work only the encoding of ZFC (and not that of CZF) has been       *)
(* developed, but it should be straightforward to do.                         *)

Require csc_eqdep.

(******************************************************************************)
(*                          Useful data types                                 *)
(******************************************************************************)

Inductive Set F := .

Inductive Set Un := void : Un.

(* Existential quantification *)
Inductive EXType [P:Type; Q:P->Prop]: Prop :=
 EXTypei : (x:P)(Q x)->(EXType P Q).

(* Sigma types -- i.e. computational existentials *)
Inductive sig [A:Type;P:A->Prop] : Type :=
 exist : (x:A)(P x)->(sig A P).

(* Existential on the Type level *)
Inductive depprod [A:Type; P : A->Type] : Type :=
 dep_i : (x:A)(P x)->(depprod A P).

(* Cartesian product in Type *)
Inductive prod_t [A,B:Type] : Type :=
 pair_t : A->B->(prod_t A B).

(******************************************************************************)
(*                         Definition of Ens, EQ, IN                          *)
(******************************************************************************)

(* The type representing sets  (Ensemble = french for set) *)
Inductive Ens : Type :=
   sup : (A:Type)(A->Ens)->Ens
 | atom : (A:Type)A->Ens.

(* Recursive Definition of the extentional equality on sets *)
Definition EQ : Ens -> Ens -> Prop.
Induction 1.
Intros A f eq1.
Induction 1.
Intros B g eq2.
Apply and.
Exact (x:A)
        (EXType ? [y:B](eq1 x (g y))).
Exact (y:B)
        (EXType ? [x:A](eq1 x (g y))).

Intros A' a'.
Exact False.

Intros A a.
Induction 1.
Intros A' f eq1.
Exact False.

Intros.
(*Exact (X == X0).*)
Exact (eq_depT Type [A:Type]A A a A0 y).
Save.

Transparent EQ.

(* Membership on sets *)
Definition IN: Ens -> Ens -> Prop :=
[E1,E2:Ens]
  Cases E2 of
    (sup A f) => (EXType ? [y:A](EQ E1 (f y)))
  | (atom A a) => False
  end.
Transparent IN.


(******************************************************************************)
(*                                  INCLUSION                                 *)
(******************************************************************************)

Definition INC : Ens -> Ens -> Prop :=
 [E1,E2:Ens]
 Cases E1 E2 of
   (sup A f)  (sup B g)  => (E:Ens)(IN E E1)->(IN E E2)
 | (sup A f)  (atom B b) => False
 | (atom A a) (sup B g)  => False      (* ??? or True?  *)
 | (atom A a) (atom B b) => (EQ E1 E2) (* ??? or False? *)
 end.

(* EQ is an equivalence relation  *)

Theorem EQ_refl : (E:Ens)(EQ E E).
Induction E.
Intros; Split; Simpl; Intro.
Exists x; Exact (H x).
Exists y; Exact (H y).
Intros; Simpl; Constructor 1.
Qed.

Theorem EQ_tran : (E1,E2,E3:Ens)(EQ E1 E2)->(EQ E2 E3)->(EQ E1 E3).
Induction E1; [Intros A1 f1 r1 | Intros A1 a1]  ;
Induction E2; [Intros A2 f2 r2 | Intros A2 a2 | Intros A2 f2 r2 | Intros A2 a2];
Induction E3; [Intros A3 f3 r3 | Auto | Contradiction | Auto |
 Auto | Contradiction | Auto | Intros A3 a3].
Simpl; Intros e1 e2; Split; Elim e1; Intros I1 I2; Elim e2; Intros I3 I4;
 [ Intros a1; Elim (I1 a1) ; Intros a2 ; Elim (I3 a2) ; Intros a3 ; Exists a3 |
   Intros a3; Elim (I4 a3) ; Intros a2 ; Elim (I2 a2) ; Intros a1 ; Exists a1 ];
 Apply r1 with (f2 a2); Assumption.

Simpl ; Intros; Inversion H; Inversion H0; Assumption.
Qed.

Theorem EQ_sym : (E1,E2:Ens)(EQ E1 E2)->(EQ E2 E1).
Induction E1 ; [ Intros A1 f1 r1 | Intros A1 a1 ];
Induction E2 ; [Intros A2 f2 r2 | Contradiction | Contradiction |Intros A2 a2].

Induction 1; Intros e1 e2; Split;
 [ Intros a2; Elim (e2 a2); Intros a1 H1; Exists a1 |
   Intros a1; Elim (e1 a1); Intros a2 H2; Exists a2 ] ; Apply r1; Assumption.
Destruct 1; Apply EQ_refl.
Qed.

Theorem EQ_INC : (E,E':Ens)(EQ E E')->(INC E E').
Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
 [Intros A' f' r' | Contradiction | Contradiction | Intros A' a'].
Simpl; Destruct 1; Intros e1 e2.
Intros C; Induction 1; Intros a ea; Elim (e1 a); Intros a' ea'; Exists a'.
Apply EQ_tran with (f a); Assumption.
Destruct 1; Hnf; Constructor 1.
Qed.

Hints Resolve EQ_sym EQ_refl EQ_INC : zfc.

Theorem INC_EQ : (E,E':Ens)(INC E E')->(INC E' E)->(EQ E E').
Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
 [Intros A' f' r' | Auto | Auto | Auto].
Unfold INC; Simpl; Intros I1 I2; Split.
Intros a; Apply I1; Exists a; Apply EQ_refl.
Intros a'; Cut (EXType A [x:A](EQ (f' a')(f x))).
Induction 1; Intros a ea; Exists a; Apply EQ_sym; Exact ea.
Apply I2; Exists a'; Apply EQ_refl.
Qed.

Hints Resolve INC_EQ : zfc.

(* Membership is extentional (i.e. is stable w.r.t. EQ)   *)

Theorem IN_sound_left :
                (E,E',E'':Ens)
                  (EQ E E')->(IN E E'')->(IN E' E'').
Induction E''; [Intros A'' f'' r'' e | Intros A'' a'' e]; Simpl.
Induction 1; Intros a'' p; Exists a''; Apply EQ_tran with E;
 [Apply EQ_sym; Assumption | Assumption].

Intro; Assumption.
Qed.

Theorem IN_sound_right :
                (E,E',E'':Ens)
                   (EQ E' E'')->(IN E E')->(IN E E'').
Induction E'; [Intros A' f' r' | Intros A' a']; Induction E'';
 [Intros A'' f'' r'' | Intros A'' a'' | Intros A'' f'' r'' | Intros A'' a''];
 Simpl.
Induction 1; Intros e1 e2; Induction 1; Intros a' e'; Elim (e1 a');
 Intros a'' e''; Exists a''; Apply EQ_tran with (f' a'); Assumption.
Intros; Assumption.
Intros; Elim H.
Intros; Assumption.
Qed.

(* Inclusion is reflexive, transitive, extentional *)

Theorem INC_refl : (E:Ens)(INC E E).
Induction E; Auto with zfc.
Qed.

Theorem INC_tran : (E,E',E'':Ens)(INC E E')->(INC E' E'')->(INC E E'').
Induction E; Induction E'; Induction E''; Simpl;
 Auto Orelse Contradiction Orelse (Intros; Elim H0; Assumption).
Qed.

Theorem INC_sound_left :
               (E,E',E'':Ens)
                  (EQ E E')->(INC E E'')->(INC E' E'').
Induction E; [Intros A f r | Intros A a]; Induction E';
 [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'];
 Induction E''; [Intros A'' f'' r'' | Contradiction | Contradiction |
 Contradiction | Contradiction | Contradiction | Contradiction |
 Intros A'' a''].
Unfold INC; Intros; Apply H0; Apply IN_sound_right with (sup A' f');
 Auto with zfc.
Destruct 1; Auto.
Qed.

Theorem INC_sound_right :
               (E,E',E'':Ens)
                 (EQ E' E'')->(INC E E')->(INC E E'').
Induction E; [Intros A f r | Intros A a]; Induction E';
 [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'];
 Induction E''; [Intros A'' f'' r'' | Contradiction | Contradiction |
 Contradiction | Contradiction | Contradiction | Contradiction |
 Intros A'' a''].
Unfold INC; Intros;  Apply IN_sound_right with (sup A' f');
 [Assumption | Apply H0; Assumption].
Destruct 1; Auto.
Qed.

(******************************************************************************)
(*                                THE EMPTY SET                               *)
(******************************************************************************)

(* The empty set  (vide = french for empty)   *)
Definition Vide : Ens :=
 (sup F [f:F]<Ens>Cases f of end).

Theorem Vide_est_vide : (E:Ens)(IN E Vide)->F.
Unfold Vide; Simpl; Intros E H; Cut False.
Induction 1.
Elim H; Intros x; Elim x.
Qed.

(* CSC: This is different from Werner *)
Theorem tout_vide_est_Vide :
 (A:Type)(f:A->Ens)((E':Ens)(IN E' (sup A f))->F)->(EQ (sup A f) Vide).
Intros; Hnf; Split.
Intro; Cut F.
Destruct 1.
Apply H with (f x); Unfold IN; Exists x; Apply EQ_refl.
Destruct y.
Qed.

(******************************************************************************)
(*                                    PAIRE                                   *)
(******************************************************************************)

Definition Paire : Ens -> Ens -> Ens :=
 [E1,E2:Ens] (sup bool [b:bool]Cases b of true => E1 | false => E2 end).

(* The pair construction is extentional *)

Theorem Paire_sound_left : (A,A',B:Ens)
                        (EQ A A')->(EQ (Paire A B)(Paire A' B)).
Unfold Paire .
Simpl.
(Intros; Split).
Induction x.
(Exists  true; Auto with zfc).

(Exists  false; Auto with zfc).

(Induction y; Simpl).
(Exists  true; Auto with zfc).

(Exists  false; Auto with zfc).
Qed.

Theorem Paire_sound_right : (A,B,B':Ens)
                (EQ B B')->(EQ (Paire A B)(Paire A B')).
Unfold Paire; Simpl; Intros; Split.
Induction x.
(Exists true; Auto with zfc).
Exists false; Auto with zfc.
Induction y.
(Exists true; Auto with zfc).
Exists false; Auto with zfc.
Qed.

Hints Resolve Paire_sound_right Paire_sound_left : zfc.

Theorem IN_Paire_left : (E,E':Ens)(IN E (Paire E E')).
Unfold Paire; Exists true; Apply EQ_refl.
Qed.

Theorem IN_Paire_right : (E,E':Ens)(IN E' (Paire E E')).
Unfold Paire; Exists false; Apply EQ_refl.
Qed.

Theorem Paire_IN : (E,E',A:Ens)(IN A (Paire E E'))->(EQ A E)\/(EQ A E').
Unfold Paire; Simpl.
Induction 1; Intros b; Elim b; Auto with zfc.
Save.

Hints Resolve IN_Paire_left IN_Paire_right Vide_est_vide : zfc.

(******************************************************************************)
(*                                  SINGLETON                                 *)
(******************************************************************************)

(* CSC: This is different from Benjamin only because I like it more; *)
(*      theorems are also simpler                                    *)
(*      In Benjamin's encoding (Sing E) was defined as (Paire E E)   *)
Definition Sing : Ens -> Ens :=
 [E:Ens] (sup Un [x:Un]Cases x of void => E end).

Theorem IN_Sing : (E:Ens)(IN E (Sing E)).
Simpl; Exists void; Apply EQ_refl.
Qed.

Theorem IN_Sing_EQ : (E,E':Ens)(IN E (Sing E'))->(EQ E E').
Simpl; Intros; Elim H; Destruct x; Trivial.
Qed.

Hints Resolve IN_Sing IN_Sing_EQ : zfc.

Theorem Sing_sound : (A,A':Ens)(EQ A A')->(EQ (Sing A)(Sing A')).
Intros; Hnf; Split; [Destruct x | Destruct y]; Exists void; Assumption.
Qed.

Hints Resolve Sing_sound : zfc.

Theorem EQ_Sing_EQ : (E1,E2:Ens)(EQ (Sing E1)(Sing E2))->(EQ E1 E2).
Intros; Hnf in H; Elim H; Intros; Elim (H0 void); Destruct x; Trivial.
Qed.

Hints Resolve EQ_Sing_EQ : zfc.

(******************************************************************************)
(*                       COMPREHENSION (OR SEPARATION)                        *)
(******************************************************************************)

Definition Comp: Ens -> (Ens -> Prop) -> Ens.
Induction 1.
Intros A f fr P.
Apply (sup {x:A|(P (f x))}).
Induction 1; Intros x p; Exact (f x).
Intros. Exact X.
Qed.

Transparent Comp.

Theorem Comp_INC : (E:Ens)(P:Ens->Prop)(INC (Comp E P) E).
Destruct E.
Intros A f P; Simpl; Destruct E0; [Intros A' f' H | Intros A' a' H];
 Elim H; Destruct x; Intros x0 p eq; Exists x0; Exact eq.
Auto with zfc.
Qed.

Theorem IN_Comp_P :
           (E,A:Ens)
               (P:Ens->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))->
                  (IN A (Comp E P))->(P A).
Induction E.
Simpl; Intros B f Hr A P H i; Elim i; Destruct x; Simpl; Intro b; Intros;
 Apply H with (f b); Auto with zfc.
Contradiction.
Qed.

Theorem IN_P_Comp :
     (E,A:Ens)
        (P:Ens ->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))->
                (IN A E)->(P A)->(IN A (Comp E P)).
Induction E.
Simpl; Intros B f HR A P H i; Elim i; Simpl; Intros; Cut (P (f x)).
Intros Pf.
Exists (exist B [x:B](P (f x)) x Pf); Simpl; Auto with zfc.
Apply H with A; Auto with zfc.
Contradiction.
Qed.

(* Again, extentionality is not stated, but easy *)

(******************************************************************************)
(*                                    UNION                                   *)
(******************************************************************************)

(* Projections of a set: *)
(*  1: its base type, F for atoms *)

Definition pi1: Ens -> Type.
Induction 1.
Intros A f r.
Exact A.
Intros.
Exact F.
Save.

Transparent pi1.

(*  2: the function, [_:F]Vide for atoms *)

Definition pi2 : (E:Ens)(pi1 E)->Ens.
Induction E.
Intros A f r.
Exact f.
Intros.
Exact Vide.
Save.

Transparent pi2.

Definition Union : (E:Ens)Ens.
Induction 1.
Intros A f r.
Apply (sup (depprod A [x:A](pi1 (f x)))).
Induction 1; Intros a b.
Exact (pi2 (f a) b).
Intros.
Exact Vide.
Save.

Transparent Union.

Theorem EQ_EXType : (E,E':Ens)
        (EQ E E')
         ->(a:(pi1 E))
            (EXType (pi1 E') [b:(pi1 E')](EQ (pi2 E a) (pi2 E' b))).
Induction E; [Intros A f r | Intros A a]; Induction E';
 [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'].
Simpl; Destruct 1; Intros e1 e2 a; Apply e1.
Contradiction.
Contradiction.
Simpl; Destruct 2.
Qed.

Transparent EQ_EXType.

Theorem IN_EXType: (E,E':Ens)(IN E' E)->
                        (EXType (pi1 E) [a:(pi1 E)](EQ E' (pi2 E a))).
Induction E.
Simpl; Intros A f r; Induction 1; Intros; Exists x; Assumption.
Destruct 1.
Qed.

Theorem IN_Union : (E,E',E'':Ens)
                (IN E' E)->(IN E'' E')->(IN E'' (Union E)).
Induction E.
2: Destruct 1.
Intros A f r.
Intros; Simpl.
Elim (IN_EXType (sup A f) E' H).
Intros x e.
Cut (EQ (pi2 (sup A f) x) E').
2: Auto with zfc v62.
Intros e1.
Cut (IN E'' (pi2 (sup A f) x)).
Intros i1.
Elim (IN_EXType ? ? i1).
Intros x0 e2.
Simpl in x0.
Exists  (dep_i A [x:A](pi1 (f x)) x x0).
Simpl.
Exact e2.
Apply IN_sound_right with E'; Assumption.
Qed.

(* CSC: This is different from Benjamin *)
Theorem IN_INC_Union :
      (A:Type)(f:A->Ens)(E:Ens)(IN (sup A f) E)->(INC (sup A f) (Union E)).
Induction E.
Intros A f r H; Hnf; Hnf in H; Intros; Elim H; Intros x e.
Cut (IN E0 (f0 x)).
Intro in_E0_f0x; Apply IN_Union with (f0 x).
Hnf; Split with x; Auto with zfc.

Auto with zfc.
Apply IN_sound_right with (sup A f); Trivial.

(Simpl; Destruct 2; Destruct x).
Qed.

Theorem Union_IN : (E,E':Ens)(IN E' (Union E))->
                                (EXType ? [E1:Ens](IN E1 E)/\(IN E' E1)).
Induction E.
2: (Simpl; Destruct 2; Destruct x).
Unfold Union ; Simpl; Intros A f r.
Induction 1.
Induction x.
(Intros a b; Simpl).
Intros.
Exists  (f a).
Split.
(Exists  a; Auto with zfc v62).

(Apply IN_sound_left with (pi2 (f a) b); Auto with zfc v62).
Simpl.
(Generalize b ; Elim (f a); Simpl).
Intros.
(Exists  b0; Auto with zfc v62).

Destruct 2.
Qed.

(* extentionality of union  *)

Theorem Union_sound
     : (E,E':Ens)(EQ E E')->(EQ (Union E) (Union E')).
Unfold Union.
Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
 [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'].

Simpl; Induction 1; Intros e1 e2; Split.
Intros x; Elim x; Intros a aa; Elim (e1 a); Intros a' ea.
Elim (EQ_EXType (f a)(f' a') ea aa); Intros aa' eaa.
Exists (dep_i A' [x:A'](pi1 (f' x)) a' aa'); Simpl; Auto with zfc v62.
Intros c'; Elim c'; Intros a' aa'; Elim (e2 a'); Intros a ea.
Cut (EQ (f' a')(f a)).
2 : Auto with zfc v62.
Intros ea'; Elim (EQ_EXType (f' a')(f a) ea' aa'); Intros aa eaa.
Exists (dep_i A [x:A](pi1 (f x)) a aa); Auto with zfc v62.

Contradiction.
Contradiction.
Destruct 1; Apply EQ_refl.
Qed.

(* The union construction is monotone w.r.t. inclusion   *)

Theorem Union_mon : (E,E':Ens)(INC E E')->(INC (Union E)(Union E')).
Induction E ; [Intros A f r | Intros A a] ; Induction E';
 [Intros A' f' r' | Contradiction | Contradiction | Intros A' a'].
2: Auto with zfc.
Intro; Cut (E:Ens)(IN E (sup A f))->(IN E (sup A' f')).
2: Auto.
Intro XXX; Cut ((E:Ens)(IN E (Union (sup A f)))->(IN E (Union (sup A' f'))))
    ->(INC (Union (sup A f)) (Union (sup A' f'))).
2: Auto.
Intros X; Apply X; Intros E0 Y; (Elim (Union_IN (sup A f) E0); Auto with zfc).
Destruct 1; Intros; Cut (IN x (sup A' f')).
2: Auto.
Intro; (Apply IN_Union with x; Auto).
Qed.

(******************************************************************************)
(*                                 INTERSECTION                               *)
(******************************************************************************)

Definition Inter : (E:Ens)Ens :=
[E:Ens]
 Cases E of
   (sup A f) =>
      (sup ?
           [c:(depprod A
	       [a:A](depprod ? [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b)(f x)))
	      )
	   ]
           Cases c of
	      (dep_i a (dep_i b p)) => (pi2 (f a) b)
	   end
      )
 | (atom A a) => Vide
 end.

Theorem IN_Inter_all : (E,E':Ens)
                        (IN E' (Inter E))->
                                (E'':Ens)(IN E'' E)->(IN E' E'').
Induction E; [Intros A f r | Contradiction]; Intros E'.
Induction 1; Intros c; Elim c; Intros a ca; Elim ca; Intros aa paa.
Intros e E'' e''.
Elim e''; Intros a1 ea1.
Apply IN_sound_right with (f a1); Auto with zfc v62.
Apply IN_sound_left with (pi2 (f a) aa); Auto with zfc v62.
Qed.

Theorem all_IN_Inter : (E,E',E'':Ens)
                         (IN E'' E)->
                            ((E'':Ens)(IN E'' E)->(IN E' E''))->
                                (IN E' (Inter E)).
(Induction E; [Intros A f r | Contradiction]).
Intros E' E'' i H.
Elim (IN_EXType (sup A f) E'' i).
(Intros a e; Simpl in a).
Simpl in e.
(Cut (IN E' E''); Auto with zfc v62).
Intros i'.
(Cut (IN E' (f a)); Auto with zfc v62).
Intros i0.
Elim (IN_EXType (f a) E' i0).
Intros b e'.
Simpl.
Cut (x:A)(IN (pi2 (f a) b) (f x)).
Intros.
Exists  (dep_i A
          [a:A]
           (depprod (pi1 (f a))
             [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)))
          a
          (dep_i (pi1 (f a))
            [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)) b H0)).
Simpl.
Auto with zfc v62.
Auto with zfc v62.
Intros.
Apply IN_sound_left with E'.
Auto with zfc v62.
Apply H.
Auto with zfc v62.
Simpl.
(Exists  x; Auto with zfc v62).
(Apply IN_sound_right with E''; Auto with zfc v62).
Qed.

(******************************************************************************)
(*                                  POWERSET                                  *)
(******************************************************************************)

Definition Power : Ens -> Ens :=
[E:Ens]
 Cases E of
  (sup A f) =>
   (sup ?
        [P:A->Prop]
	    (sup ?
	         [c:(depprod A [a:A](P a))]
		    Cases c of
		      (dep_i a p) => (f a)
		    end
            )
   )
 | (atom A a) => (Sing (atom A a)) (* ??? or Vide? *)
 end.

Theorem IN_Power_INC : (E,E':Ens)(IN E' (Power E))->(INC E' E).
Induction E.
Intros A f r; Unfold INC ; Simpl.
Intros E'; Induction 1; Intros P.
Elim E'.
Simpl.
Intros A' f' r'.
Induction 1; Intros HA HB.
Intros E''; Induction 1; Intros a' e.
Elim (HA a').
Induction x; Intros a p.
Intros; Exists  a.
Apply EQ_tran with (f' a'); Auto with zfc v62.
Contradiction.
Auto with zfc.
Qed.

(* CSC: This is different from Benjamin *)
Theorem INC_IN_Power : (E,E':Ens)(INC E' E)->(IN E' (Power E)).
Induction E.
2: Induction E'.
2: Contradiction.
2: (Destruct 1; Unfold Power; Auto with zfc).
Intros A f r; Unfold INC; Simpl; Induction E'.
2: Contradiction.
Intros A' f' r' i.
Exists  [a:A](IN (f a) (sup A' f')).
Simpl.
Split.
Intros.
Elim (i (f' x)).
Intros a e.
(Cut (EQ (f a) (f' x)); Auto with zfc v62).
Intros e1.
Exists  (dep_i A [a:A](EXType A' [y:A'](EQ (f a) (f' y))) a
          (EXTypei A' [y:A'](EQ (f a) (f' y)) x e1)).
Auto with zfc v62.
Simpl.
(Exists  x; Auto with zfc v62).
Induction y; Induction 1; Intros.
(Exists  x0; Auto with zfc v62).
Qed.

Theorem Power_mon : (E,E':Ens)(INC E E')->(INC (Power E)(Power E')).
Induction E; [Intros A f r | Intros A a]; Induction E';
 [Intros A' f' r' | Contradiction | Contradiction | Destruct 1; Auto with zfc].
Intro.
Hnf in H.
Cut ((E:Ens)(IN E (Power (sup A f)))->(IN E (Power (sup A' f'))))
    ->(INC (Power (sup A f)) (Power (sup A' f'))).
2: Auto.
Intros.
Apply H0.
Intros.
Cut (INC E0 (sup A f)).
2: (Apply IN_Power_INC; Auto).
Intro.
Cut (INC E0 (sup A' f')).
Intro.
Apply INC_IN_Power.
Assumption.

Generalize H2.
Elim E0.
Unfold INC.
Auto with zfc.

Auto with zfc.
Qed.

Theorem Power_sound : (E,E':Ens)(EQ E E')->(EQ (Power E)(Power E')).
Induction E; [Intros A f r | Intros A a]; Induction E';
 [Intros A' f' r' | Contradiction | Contradiction | Destruct 1; Auto with zfc].
Intro.
Apply INC_EQ.
Cut ((E:Ens)(IN E (Power (sup A f)))->(IN E (Power (sup A' f'))))
    ->(INC (Power (sup A f)) (Power (sup A' f'))).
2: Auto.
Intros; Apply H0; Clear H0; Intros; Cut (INC E0 (sup A f)).
2: (Apply IN_Power_INC; Auto with zfc).
Clear H0; Intro; Apply INC_IN_Power.
(Apply INC_sound_right with (sup A f); Auto).

(* Using simmetry *)
Cut ((E:Ens)(IN E (Power (sup A' f')))->(IN E (Power (sup A f))))
    ->(INC (Power (sup A' f')) (Power (sup A f))).      
2: Auto. 
Intros; Apply H0; Clear H0; Intros; Cut (INC E0 (sup A' f')).
2: (Apply IN_Power_INC; Auto with zfc).
Clear H0; Intro; Apply INC_IN_Power.
(Apply INC_sound_right with (sup A' f'); Auto with zfc).
Qed.

(******************************************************************************)
(*                              ORDERED COUPLES                               *)
(******************************************************************************)

(* small lemmas *)

Theorem not_EQ_Sing_Vide : (E:Ens)(EQ (Sing E) Vide)->F.
Intros E e; Cut False.
Induction 1.
Cut (IN E Vide).
Simpl; Induction 1; Intros xx; Elim xx; Induction 1.
Apply IN_sound_right with (Sing E); Auto with zfc v62.
Qed.

Theorem not_EQ_Vide_Sing : (E:Ens)(EQ Vide (Sing E))->F.
Intros E e; Cut False.
Induction 1.
Cut (IN E Vide).
Simpl; Induction 1; Intros xx; Elim xx; Induction 1.
Apply IN_sound_right with (Sing E); Auto with zfc v62.
Qed.

(* This definition of the ordered pair is slightly different from *)
(* the usual one, since we want it to work in an intuisionistic   *)
(* setting. Works the same, neitherless. The soundness proofs are *)
(* unpleasant.                                                    *)

Definition Couple := [E,E': Ens](Paire (Sing E) (Paire Vide (Sing E'))).

Theorem Couple_inj_left : (A,A',B,B':Ens)
                (EQ (Couple A A')(Couple B B'))->(EQ A B).
(Unfold Couple; Simpl); Induction 1; (Intros HA HB; Elim (HA true)).
(Intros x; Elim x; Simpl; Induction 1; Intros H3 H4; Elim (H3 void);
 Simpl; Destruct x0).
Trivial.

Elim (H4 false); Destruct x1; Intros; Cut (EQ (Sing B') Vide).
Simpl; Induction 1; Intros yy; Elim (yy void); Destruct x2.

Apply EQ_tran with A.
Auto with zfc.

Assumption.

Intros; Cut (EQ (Sing B') Vide).
Simpl; Induction 1; Intros yy; Elim (yy void); Destruct x1.

Apply EQ_tran with A.
Auto with zfc.

Elim (H4 true); Destruct x1; Trivial.
Qed.

Theorem Couple_inj_right :  (A,A',B,B':Ens)
                (EQ (Couple A A')(Couple B B'))->(EQ A' B').
Unfold Couple; Simpl.
Induction 1; Intros H1 H2.
Elim (H1 false).
Intros bb1; Elim bb1.
Intros HF.
Change (EQ (Paire Vide (Sing A'))(Sing B)) in HF.
Cut F.
Induction 1.
Apply (not_EQ_Vide_Sing A').
Apply EQ_tran with B.
Apply IN_Sing_EQ; Apply IN_sound_right with (Paire Vide (Sing A'));
 Auto with zfc v62.
Apply EQ_sym; Apply IN_Sing_EQ;
        Apply IN_sound_right with (Paire Vide (Sing A')); Auto with zfc v62.
Change (EQ (Paire Vide (Sing A'))(Paire Vide (Sing B')))->(EQ A' B').
Intros HP; Cut (EQ (Sing A') (Sing B')).
Intros; Auto with zfc v62.
Cut (IN (Sing A')(Paire Vide (Sing B'))).
Intros HI; Elim (Paire_IN Vide (Sing B')(Sing A') HI).
Intros; Cut F.
Induction 1.
Apply not_EQ_Sing_Vide with A'; Assumption.
Trivial with zfc v62.
Apply IN_sound_right with (Paire Vide (Sing A')); Auto with zfc v62.
Qed.

(******************************************************************************)
(*                                   POWERSET                                 *)
(******************************************************************************)

(* Here we cheat. It is easier to define the cartesian product using    *)
(* the type theoretical product, i.e. we here use non set-theoretical   *)
(* constructions. We could however use the usual definitions.           *)

Definition Prod : Ens -> Ens -> Ens :=
[E,E':Ens]
 Cases E E' of
   (sup A f) (sup A' f') =>
     (sup ?
          [c:(prod_t A A')]
	       Cases c of
	         (pair_t a a') => (Couple (f a) (f' a'))
	       end
     )
 | _ _ => Vide
 end.

Hints Resolve Paire_sound_left Paire_sound_right : zfc.

Theorem Couple_sound_left :
        (A,A',B:Ens)(EQ A A')->(EQ (Couple A B)(Couple A' B)).
 Unfold Couple;Intros; Auto with zfc v62.
Save.

Theorem Couple_sound_right:
        (A,B,B':Ens)(EQ B B')->(EQ (Couple A B)(Couple A B')).
 Unfold Couple;Intros; Auto with zfc v62.
Save.

Theorem Couple_IN_Prod : (E1,E2,E1',E2':Ens)
                (IN E1' E1)->(IN E2' E2)->
                        (IN (Couple E1' E2')(Prod E1 E2)).
Induction E1; [Intros A1 f1 r1 | Contradiction].
Induction E2; [Intros A2 f2 r2 | Contradiction].
Intros E1' E2' i1 i2.
Elim (IN_EXType (sup A1 f1) E1').
(Intros x e1; Simpl in x).
Elim (IN_EXType (sup A2 f2) E2').
(Intros x0 e2; Simpl in x).
Apply IN_sound_left with (Couple (pi2 (sup A1 f1) x) (pi2 (sup A2 f2) x0)).
Apply EQ_tran with (Couple (pi2 (sup A1 f1) x) E2').
Apply Couple_sound_right.
Auto with zfc v62.

(Apply Couple_sound_left; Auto with zfc v62).

Simpl.
Exists  (pair_t ? ? x x0).
Simpl.
Split.

Induction x1.
Exists true; Auto with zfc.
Exists false; Auto with zfc.

Induction y.
Exists true; Auto with zfc.
Exists false; Auto with zfc.
Assumption.
Assumption.
Qed.

Theorem Couple_Prod_IN :  (E1,E2,E1',E2':Ens)
                (IN (Couple E1' E2')(Prod E1 E2))->
                        (IN E1' E1)/\(IN E2' E2).
Induction E1; [Intros A1 f1 r1 | Destruct 1; Destruct x].
Induction E2; [Intros A2 f2 r2 | Destruct 1; Destruct x].
Intros E1' E2' i.
Elim (IN_EXType (Prod (sup A1 f1) (sup A2 f2)) (Couple E1' E2') i).
Destruct x; Intros a1 a2 e.
Change (EQ (Couple E1' E2') (Couple (f1 a1) (f2 a2))) in e.
Cut (EQ E1' (f1 a1)).
Cut (EQ E2' (f2 a2)).
Intros e1 e2.
Split.
Apply IN_sound_left with (f1 a1); Auto with zfc v62; Simpl; Exists a1;
 Auto with zfc v62.
Apply IN_sound_left with (f2 a2); Auto with zfc v62; Simpl; Exists  a2;
 Auto with zfc v62.
Apply Couple_inj_right with A:=E1' B:=(f1 a1); Auto with zfc v62.
Apply Couple_inj_left with E2' (f2 a2); Auto with zfc v62.
Qed.

Theorem IN_Prod_EXType : (E,E',E'':Ens)(IN E'' (Prod E E'))->
        (EXType ? [A:Ens](EXType ? [B:Ens](EQ (Couple A B) E''))).
Induction E ; [Intros A  f  r  | Destruct 1; Destruct x].
Induction E'; [Intros A' f' r' | Destruct 1; Destruct x].
Intros; Elim (IN_EXType (Prod (sup A f) (sup A' f')) E'').
Induction x.
Intros; Exists  (f y); Exists  (f' y0); Auto with zfc v62.
Auto with zfc v62.
Qed.

(******************************************************************************)
(*                                  ORDINALS                                  *)
(******************************************************************************)

Definition Succ := [E:Ens](Union (Paire E (Sing E))).

Inductive Ord : Ens -> Prop :=
  Oo : (Ord Vide)
| So : (E:Ens)(Ord E)->(Ord (Succ E))
| Lo : (E:Ens)((e:Ens)(IN e E)->(Ord e))->(Ord (Union E))
| Eo : (E,E':Ens)(Ord E)->(EQ E E')->(Ord E').

Hints Resolve Oo So Lo : zfc.

Definition Nat : nat ->Ens.
Induction 1; Intros.
Exact Vide.
Exact (Succ X).
Save.

Transparent Nat.

Theorem Nat_Ord : (n:nat)(Ord (Nat n)).
Induction n; Simpl; Auto with zfc v62.
Save.

Definition Omega : Ens :=
  (sup nat Nat).

Theorem IN_Succ :  (E:Ens)(IN E (Succ E)).
Intros E; Unfold Succ; Apply IN_Union with (Sing E); Auto with zfc v62.
Qed.

(* CSC: This is different from Werner *)
Theorem INC_Succ : (A:Type)(f:A->Ens)(INC (sup A f) (Succ (sup A f))).
Intros; Cut ((E:Ens)(IN E (sup A f))->(IN E (Succ (sup A f))))
    ->(INC (sup A f) (Succ (sup A f))).
Intros; Apply H; Unfold Succ; Intros.
Apply IN_Union with (sup A f); Auto with zfc.

Intros; Exact H.
Qed.

Hints Resolve IN_Succ INC_Succ : zfc.

Theorem IN_Succ_or : (E,E':Ens)(IN E' (Succ E))->(EQ E E')\/(IN E' E).
Intros E E' i.
Unfold Succ  in i.
Elim (Union_IN (Paire E (Sing E)) E' i).
Intros E1; Induction 1; Intros i1 i2.
Elim (Paire_IN E (Sing E) E1 i1).
Intros; Right; Apply IN_sound_right with E1; Auto with zfc v62.
Intros; Left; Cut (IN E' (Sing E)).
Auto with zfc v62.
Apply IN_sound_right with E1; Auto with zfc v62.
Qed.

Theorem E_not_IN_E : (E:Ens)(IN E E)->F.
Induction E.
Intros A f r i.
Cut False.
Induction 1.
Elim (IN_EXType (sup A f) (sup A f) i); Intros a e.

Simpl in a.
Change (EQ (sup A f) (f a)) in e.
Elim (r a).
Apply IN_sound_right with (sup A f); Auto with zfc v62.
Exists a; Auto with zfc v62.
Intros; Cut False; Contradiction.
Qed.

Theorem Nat_IN_Omega : (n:nat)(IN (Nat n) Omega).
Intros; Simpl; Exists n; Auto with zfc v62.
Qed.
Hints Resolve Nat_IN_Omega : zfc.

Theorem IN_Omega_EXType : (E:Ens)(IN E Omega)->(EXType ? [n:nat](EQ (Nat n) E)).
(Simpl; Induction 1).
Intros n e.
(Exists  n; Auto with zfc v62).
Qed.

Theorem IN_Nat_EXType : (n:nat)(E:Ens)(IN E (Nat n))->(EXType ? [p:nat](EQ E (Nat p))).
Induction n.
Simpl.
Induction 1.
Induction x.

Intros.
Change (IN E (Succ (Nat n0))) in H0.
Elim (IN_Succ_or (Nat n0) E H0).
(Intros; Exists  n0).
Auto with zfc v62.

Intros.
(Elim (H E); Auto with zfc v62).
Qed.

Theorem Omega_EQ_Union : (EQ Omega (Union Omega)).
Apply INC_EQ.
Cut ((E:Ens)(IN E Omega)->(IN E (Union Omega)))
    ->(INC Omega (Union Omega)).
Intros; Apply H.
Clear H.
Intros.
Elim (IN_Omega_EXType E H).
Intros n e.
Apply IN_Union with (Nat (S n)).
Auto with zfc v62.

Apply IN_sound_left with (Nat n).
Auto with zfc v62.

(Change (IN (Nat n) (Succ (Nat n))); Auto with zfc v62).

Intros.
Exact H.

Cut ((E:Ens)(IN E (Union Omega))->(IN E Omega))
    ->(INC (Union Omega) Omega).
Intros; Apply H; Clear H.
Intros.
Elim (Union_IN Omega E H).
Intros e h.
Elim h.
Intros i1 i2.
Elim (IN_Omega_EXType e i1).
Intros n e1.
Cut (IN E (Nat n)).
Intros.
(Elim (IN_Nat_EXType n E H0); Intros).
(Apply IN_sound_left with (Nat x); Auto with zfc v62).

(Apply IN_sound_right with e; Auto with zfc v62).

Intros.
Exact H.
Qed.

Theorem Omega_Ord : (Ord Omega).
Apply Eo with (Union Omega).
Apply Lo.
Intros.
Elim (IN_Omega_EXType e H).
Intros n ee.
Apply Eo with (Nat n); Auto with zfc v62.
Elim n.
Auto with zfc v62.
Auto with zfc v62.
Intros.
Change (Ord (Succ (Nat n0))); Auto with zfc v62.
Apply EQ_sym; Auto with zfc v62.
Apply Omega_EQ_Union.
Qed.

Definition Alpha : Ens->Ens.
Induction 1.
Intros A f r.
Apply Union.
Apply (sup A).
Intros a.
Exact (Power (r a)).
Intros A a; Exact (atom A a). (* ??? or Vide? *)
Save.

Transparent Alpha.

(******************************************************************************)
(*                           AXIOM OF CHOICE                                  *)
(******************************************************************************)

(* A Type-theoretical axiom of choice gives us the collection axiom  *)

Definition collection :=
 (P:Ens->Ens->Prop)
  ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))->
   ((E:Ens)(EXType ? (P E)))->
     (E:Ens)(EXType ? [A:Ens](x:Ens)(IN x E)->
      (EXType ? [y:Ens](IN y A)/\(P x y))).


Definition choice :=
 (A,B:Type)(P:A->B->Prop)
   ((a:A)(EXType ? [b:B](P a b)))->
       (EXType ? [f:A->B]((a:A)(P a (f a)))).

Theorem Choice_Collection : choice -> collection.
Intro; Unfold collection; Intros P comp G E;
 Cut (EXType ? [f:(Ens->Ens)](B:Ens)(P B (f B))).
Induction 1; Intros f Pf; Elim E.
Intros A g hr; Split with (sup A [a:A](f (g a))).
Simpl; Intros X i; Elim i; Intros a ea; Split with (f (g a)).
Split.
Exists a; Auto with zfc.

Apply comp with (g a); Auto with zfc.

Auto with zfc.

Intros; Split with Vide; Contradiction.

Unfold choice in H; Apply H; Intros; Elim (G a); Intros b hb; Exists b;
 Assumption.
Qed.

(* If we also assume the excluded middle, we can derive         *)
(* the usual replacement schemata.                              *)

Definition functional :=
        [P:Ens->Ens->Prop](x,y,y':Ens)
                (P x y)->(P x y')->(EQ y y').
Definition replacement :=
   (P:Ens->Ens->Prop)
        (functional P)->
        ((x,y,y':Ens)(EQ y y')->(P x y)->(P x y'))->
        ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))->
       (X:Ens)(EXType ? [Y:Ens](y:Ens)
                            (((IN y Y)->(EXType ? [x:Ens](IN x X)/\(P x y)))
                            /\((EXType ? [x:Ens](IN x X)/\(P x y))->(IN y Y)))).

Theorem classical_Collection_Replacement :
 ((S:Prop)S\/(S->False))->
        collection ->
                replacement.
Unfold replacement; Intros EM Collection P fp comp_r comp_l X.
Cut (EXType ? [Y:Ens](y:Ens)((EXType ? [x:Ens](IN x X)/\(P x y))->(IN y Y))).
Induction 1; Intros Y HY.
Exists (Comp Y [y:Ens](EXType ? [x:Ens](IN x X)/\(P x y))).
Intros y; Split.
Intros HC.
Apply (IN_Comp_P Y y [y0:Ens](EXType Ens [x:Ens](IN x X)/\(P x y0))); Auto with zfc v62.
Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e.
Exists x; Split; Auto with zfc v62.
Apply comp_r with w1; Auto with zfc v62.
Intros He.
Apply IN_P_Comp.

Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e.
Exists x; Split; Auto with zfc v62.
Apply comp_r with w1; Auto with zfc v62.
Apply HY; Auto with zfc v62.
Auto with zfc v62.

Elim (Collection [x,y:Ens]((P x y)\/(((y':Ens)(P x y')->False)/\(EQ y Vide))))
        with X.
Intros Y HY.
Elim (EM (EXType ? [x:Ens](IN x X)/\(P x Vide))).
Intros Hvide; Elim Hvide; Intros xv Hxv; Exists Y.
Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2.
Elim (HY x Hx1).
Intros y'; Induction 1; Intros Hy'1 Hy'2.
Elim Hy'2.
Intros Hy'3; Apply IN_sound_left with y'; Auto with zfc v62.
Apply fp with x; Auto with zfc v62.
Induction 1; Intros Hy'3 Hy'4.
Elim (Hy'3 y Hx2).
Intros HP; Exists (Comp Y [y:Ens]((EQ y Vide)->False)).
Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2.
Apply IN_P_Comp.
Intros w1 w2 Hw1 Hw Hw2; Apply Hw1; Apply EQ_tran with w2; Auto with zfc v62.
Elim (HY x).
Intros y'; Induction 1; Intros Hy'1 Hy'2.
Elim Hy'2; Intros Hy'3.
Apply IN_sound_left with y'; Auto with zfc v62.
Apply fp with x; Auto with zfc v62.
Elim Hy'3; Intros Hy'4 Hy'5.
Elim (Hy'4 y); Auto with zfc v62.
Assumption.
Intros e; Apply HP; Exists x; Split; Auto with zfc v62;
        Apply comp_r with y; Auto with zfc v62; Apply fp; Auto with zfc v62.
Intros x x' y e Hx; Elim Hx; Intros Hx1.
Left; Apply comp_l with x; Auto with zfc v62.
Right; Elim Hx1; Intros Hx2 Hx3; Split.
2 : Assumption.
Intros y' Hy'; Apply (Hx2 y'); Apply comp_l with x'; Auto with zfc v62.
Intros x; Elim (EM (EXType ? [y:Ens](P x y))); Intros Hx.
Elim Hx; Intros x0 Hx0; Exists x0; Left; Assumption.
Exists Vide; Right; Split; Auto with zfc v62.
Intros y Hy; Elim Hx; Exists y; Auto with zfc v62.
Qed.

(******************************************************************************)
(*                  SMALL SETS AND THE BIG SET OF SMALL SETS                  *)
(******************************************************************************)

(* Some definitions replicated on another type level *)

Inductive EXType' [P:Type; Q:P->Prop]: Prop :=
 EXTypei' : (x:P)(Q x)->(EXType' P Q).

Inductive prod_t' [A,B:Type] : Type :=
 pair_t' : A->B->(prod_t' A B).

Inductive depprod'' [A:Type; P : A->Type] : Type :=
 dep_i'' : (x:A)(P x)->(depprod'' A P).

(* The small sets  *)
Inductive Ens' : Type :=
   sup' : (A:Type)(A->Ens')->Ens'
 | atom' : (A:Type)A->Ens'.

(* Equality on small sets *)
Definition EQ' : Ens' -> Ens' -> Prop.
Induction 1.
Intros A f eq1.
Induction 1.
Intros B g eq2.
Apply and.
Exact (x:A)
        (EXType' ? [y:B](eq1 x (g y))).
Exact (y:B)
        (EXType' ? [x:A](eq1 x (g y))).

Intros A' a'.
Exact False.

Intros A a.
Induction 1.
Intros A' f eq1.
Exact False.

Intros.
(*Exact (X == X0).*)
Exact (eq_depT Type [A:Type]A A a A0 y).
Save.

Transparent EQ'.

(* small sets can be injected into big sets *)
Definition inj : Ens'->Ens.
Induction 1; [Intros A f fr ; Exact (sup A fr) | Intros A a ; Exact (atom A a)].
Qed.

Transparent inj.

Theorem inj_sound : (E1,E2:Ens')(EQ' E1 E2)->(EQ (inj E1)(inj E2)).
Induction E1; [Intros A1 f1 r1 | Intros A a] ; Induction E2;
 [Intros A2 f2 r2 | Contradiction | Contradiction | Intros A' a'].
(Induction 1; Intros HR1 HR2; Split).
(Intros a1; Elim (HR1 a1); Intros a2 Ha2; Exists  a2; Auto with zfc v62).
(Intros a2; Elim (HR2 a2); Intros a1 Ha1; Exists  a1; Auto with zfc v62).

Auto with zfc.
Qed.

Definition Sing' : Ens' -> Ens' :=
 [E:Ens'] (sup' Un [x:Un]Cases x of void => E end).

Definition Power' : Ens' -> Ens' :=
[E:Ens']
 Cases E of
  (sup' A f) =>
   (sup' ?
        [P:A->Prop]
	    (sup' ?
	         [c:(depprod'' A [a:A](P a))]
		    Cases c of
		      (dep_i'' a p) => (f a)
		    end
            )
   )
 | (atom' A a) => (Sing' (atom' A a)) (* ??? or Vide? *)
 end.

Theorem Power_sound_inj : (E:Ens')(EQ (inj (Power' E))(Power (inj E))).
Induction E; [Intros A f HR | Intros A a].
Simpl; Split.
Intros P; Exists P; Split.
Intros c; Elim c; Intros a p.
Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
Intros c; Elim c; Intros a p.
Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
Intros P; Exists P; Split.
Intros c; Elim c; Intros a p.
Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
Intros c; Elim c; Intros a p.
Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto with zfc v62.

Simpl; Split.
Destruct x; Exists void; Auto with zfc.
Destruct y; Exists void; Auto with zfc.
Qed.

(* The set of small sets *)
Definition Big := (sup Ens' inj).

Theorem Big_is_big : (E:Ens')(IN (inj E) Big).
Intros E; Unfold Big; Simpl; Exists E; Auto with zfc.
Qed.

Theorem IN_Big_small : (E:Ens)(IN E Big)->(EXType' ? [E':Ens'](EQ E (inj E'))).
Unfold Big; Simpl; Induction 1; Intros E' HE'; Exists E'; Assumption.
Qed.

Theorem IN_small_small : (E:Ens)(E':Ens')(IN E (inj E'))->
                (EXType' ? [E1:Ens'](EQ E (inj E1))).
Induction E'; [Intros A' f' HR' | Contradiction]; Simpl;
        Induction 1; Intros a' e'; Exists  (f' a'); Assumption.
Qed.

Theorem Big_closed_for_power : (E:Ens)(IN E Big)->(IN (Power E) Big).
Unfold Big; Simpl; Intros E; Induction 1; Intros E' HE'; Exists (Power' E').
Apply EQ_tran with (Power (inj E')).
Apply Power_sound; Assumption.
Apply EQ_sym; Apply Power_sound_inj.
Qed.

(******************************************************************************)
(*                            NO SET OF ALL SETS                              *)
(******************************************************************************)

(* Just for fun : a proof that there is no set of all sets, using *)
(* Russell's paradox construction                                 *)
(* There, of course, are other proofs (foundation, etc)           *)

Theorem Russell : (E:Ens)((E':Ens)(IN E' E))->False.
Intros U HU.
Cut ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)).
Intros HR.
Apply HR.
(Apply IN_P_Comp; Auto with zfc v62).
(Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto with zfc v62;
 Apply IN_sound_right with w2; Auto with zfc v62).
Intros H.
Cut (IN (Comp U [x:Ens](IN x x)->False) (Comp U [x:Ens](IN x x)->False)).
Change ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)).
Cut (w1,w2:Ens)((IN w1 w1)->False)->(EQ w1 w2)->(IN w2 w2)->False.
Intros ww.
Exact (IN_Comp_P U (Comp U [x:Ens](IN x x)->False)
        [x:Ens](IN x x)->False ww H).
(Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto with zfc v62;
 Apply IN_sound_right with w2; Auto with zfc v62).
Assumption.
Qed.

(******************************************************************************)
(*                     SOME AXIOMS AND STRANGE THINGS ;-(                     *)
(*                                                                            *)
(*  The need for axioms is due to the usage of dependent equality, or to my   *)
(*  ignorance about it ;-)                                                    *)
(*                                                                            *)
(******************************************************************************)

Axiom a_de_pi2 :
 (T:Type)(n,m:T)(existT Type [A:Type]A T n)==(existT Type [A:Type]A T m)->n==m.

(* The main consequence of the previous axiom *)
Theorem a_pi2 : (T:Type)(n,m:T)(atom T n)==(atom T m)->n==m.
Intros; Inversion H; Apply a_de_pi2; Assumption.
Qed.

(* This theorem is really strange: I can prove this in general, but I can't  *)
(* prove any of it's instance: for example I can't prove                     *)
(* ~(nat==bool)->~(atom nat O)==(atom bool true) due to an internal error of *)
(* Coq                                                                       *)
Theorem a_npi1 : (T1,T2:Type)(t1:T1)(t2:T2)~T1==T2->~(atom T1 t1)==(atom T2 t2).
Unfold not; Intros; Apply H; Inversion H0; Reflexivity.
Qed.

(******************************************************************************)
(*                  MAPPING A TYPE TO THE SET OF IT'S ELEMENTS                *)
(******************************************************************************)

(* (Ens_of_t T t) is thought as the coercion from an element (t:T) to a set *)
Definition Ens_of_t : (T:Type)T->Ens :=
 [T:Type][t:T](atom T t).

(* (Ens_of_T T) is thought as the set of the elements of type T ... *)
Definition Ens_of_T : Type -> Ens :=
 [T:Type] (sup T [t:T](Ens_of_t T t)).

(* ... and (Prop_on_Ens_of_Prop T P) is thought as the proposition on Ens *)
(* that is true only for (atom T t) where (t:T) and (P t) is true.        *)
Inductive Prop_on_Ens_of_Prop [T:Type; P:T->Prop] : Ens->Prop :=
  cons : (t:T)(P t)->(Prop_on_Ens_of_Prop T P (atom T t)).

Theorem Prop_on_Ens_of_Prop_atom_Prop :
   (T:Type; P:(T->Prop); t:T)(Prop_on_Ens_of_Prop T P (atom T t))->(P t).
Intros; Inversion H; Replace t with t0.
Assumption.

Apply a_de_pi2; Assumption.
Qed.

Theorem Prop_on_Ens_of_Prop_t :
  (T:Type; P:(T->Prop); E:Ens)
        (Prop_on_Ens_of_Prop T P E)
        ->(EXType T [t:T]E==(atom T t)/\(P t)).
Intros.
Inversion H.
Split with t.
Auto.
Qed.

Lemma EQ_atom: (T:Type)(t:T)(E:Ens)(EQ (atom T t) E)->(atom T t)==E.
Destruct E.
Contradiction.

Intros.
Inversion H.
Reflexivity.
Qed.


Theorem Prop_on_Ens_of_Prop_sound :
   (E1,E2:Ens)(T:Type)(P:T->Prop)
    (EQ E1 E2)
    -> (Prop_on_Ens_of_Prop T P E1)
    -> (Prop_on_Ens_of_Prop T P E2).
Intros.
Cut (EXType ? [t:T]E1==(atom T t)/\(P t)).
Destruct 1; Destruct 1.
Intros.
Rewrite H3 in H.
Cut (atom T x)==E2.
Intros.
Rewrite <- H5.
Constructor 1.
Assumption.

Apply EQ_atom.
Assumption.

Apply Prop_on_Ens_of_Prop_t.
Assumption.
Qed.


(******************************************************************************)
(*                             EXAMPLES OF USAGE                              *)
(******************************************************************************)

(* We could define an implicit coercion from nat to Ens using Ens_of_t *)
Coercion Ens_of_nat := [n:nat](Ens_of_t nat n).

(* CNat is the set of the natural numbers of Coq ... *)
Definition CNat : Ens :=
 (Ens_of_T nat).

Mutual Inductive
 is_even : nat->Prop :=
    is_even_O : (is_even O)
  | is_even_S : (n:nat)(is_odd n)->(is_even (S n))
with
 is_odd : nat->Prop :=
    id_ood_S : (n:nat)(is_even n)->(is_odd (S n)).

Lemma not_even_odd: (n:nat)(is_even n)->(is_odd n)->False.
Induction n.
Intros; Inversion H0.

Intros; Apply H; [Inversion H1 | Inversion H0]; Assumption.
Qed.

Definition Cis_even : Ens -> Prop :=
  (Prop_on_Ens_of_Prop nat is_even).

Definition Cis_odd : Ens -> Prop :=
  (Prop_on_Ens_of_Prop nat is_odd).

(* ... and CEven and COdd are the sets of even/odd natural numbers of Coq *)

Definition CEven := (Comp CNat Cis_even).

Definition COdd  := (Comp CNat Cis_odd).

(* And now an easy fact: the intersection of CEven with COdd is empty *)
Fact COdd_Inter_CEven_EQ_Vide: (EQ (Inter (Paire CEven COdd)) Vide).
Apply INC_EQ.    
Cut (E:Ens)(IN E (Inter (Paire CEven COdd)))->(IN E Vide).
Auto.

Intros.
Cut False.
Contradiction.

Cut (IN E CEven)/\(IN E COdd).
Destruct 1.
Intros.
Unfold CEven in H1.
Cut (Cis_even E).
Unfold COdd in H2.
Cut (Cis_odd E).
Intros.
Inversion H3.
Inversion H4.
Rewrite <- H6 in H8.
Cut t0==t.
Intro.
Rewrite H9 in H7.
Apply not_even_odd with t; Assumption.

Apply a_pi2; Assumption.

Apply IN_Comp_P with CNat.
Intros.
Unfold Cis_odd.
Apply Prop_on_Ens_of_Prop_sound with w1; Assumption.

Assumption.

Apply IN_Comp_P with CNat.
Intros.
Unfold Cis_even.
Apply Prop_on_Ens_of_Prop_sound with w1; Assumption.

Assumption.

Split.
Apply IN_Inter_all with (Paire CEven COdd).
Assumption.

Auto with zfc.

Apply IN_Inter_all with (Paire CEven COdd).
Assumption.

Auto with zfc.

Simpl.
Destruct 1.
Destruct x.
Qed.

(* Another easy fact: O is not in COdd *)
Fact O_not_IN_COdd : ~(IN O COdd).
Unfold not; Intro.
Cut (Cis_odd O).
Intro.
Inversion H0.
Simpl in H1.
Cut t==O.
Intro.
Rewrite H3 in H2.
Inversion H2.

Apply a_de_pi2.
Assumption.

Unfold COdd in H.
Apply IN_Comp_P with CNat.
Intros.
Unfold Cis_odd.
Apply Prop_on_Ens_of_Prop_sound with w1.
Assumption.

Exact H0.

Assumption.
Qed.