(*** file groundwork7.v, version of october 22nd, 2003---Carlos Simpson ***)


Set Implicit Arguments.

Require Arith.

Module Axioms.

(************************ PARAMETERS AND AXIOMS ************************)

(*** interpret types as being classical sets ***)

Definition E := Type.

(*** elements of a set are themselves sets ***)

(***) Parameter R : (x:E)x -> E.  
(***) Axiom R_inj : (x:E; a,b:x)(R a) == (R b) -> a == b.

Definition inc := [x,y:E](exT ? [a:y](R a) == x).

Definition sub := [a,b:E](x:E)(inc x a) -> (inc x b).


(*** a set is determined by its elements ****)

(***) Axiom extensionality : (a,b:E)(sub a b) -> (sub b a) -> a == b.


(*** we also need extensionality for general product types ***)

(***) Axiom prod_extensionality : (x:Type; y: x -> Type; u,v: (a:x)(y a))
((a:x)(u a) == (v a)) -> u == v.

Lemma arrow_extensionality : (x,y:Type; u,v:x->y)((a:x)(u a) == (v a)) -> u == v.
Intros x y.
Change (u,v:(a:x)([i:x]y a))((a:x)(u a)==(v a))->u==v.
Intros. Apply prod_extensionality. Assumption.
Save. 


Inductive nonemptyT [t:Type] : Prop := 
nonemptyT_intro : t -> (nonemptyT t).

Inductive exists [p:E -> Prop]: Prop :=
exists_intro : (x:E)(p x) -> (exists p).
Inductive nonempty [x: E] : Prop := 
nonempty_intro : (y:E)(inc y x) -> (nonempty x).

(*** the axiom of choice on the type level *********************
WARNING: !!!!!!!!!!! this version of choice is contradictory with 
the impredicativity of Set; when using things like nat : Set, be careful
not to invoke the impredicativity of Set !!!!!!!!!!!!!! *********)

(***) Parameter chooseT :(t:Type; p: t-> Prop)(nonemptyT t) -> t.
(***) Axiom chooseT_pr : (t:Type; p: t-> Prop; ne: (nonemptyT t))
(exT ? p)-> (p (chooseT p ne)).


(*** the replacement axiom: images of a set are again sets *********)

(***) Parameter IM : (x:E)(x -> E) -> E.
(***) Axiom IM_exists : (x:E; f:x -> E; y:E)(inc y (IM f)) -> (exT ? [a:x](f a) == y).
(***) Axiom IM_inc : (x:E; f:x -> E; y:E)(exT ? [a:x](f a) == y) ->
(inc y (IM f)). 

(*** the following actually follow from the above as was shown in the
standard library but we write them as axioms for brevity **************)

(***) Axiom excluded_middle : (P:Prop)(not (not P)) -> P.
(***) Axiom proof_irrelevance : (P:Prop; q,p:P)p==q.

(*** the following axioms can be obtained from the Ensembles library but we include it here
as an axiom; it is used for convenience, allowing us to replace iff by equality so as to
be able to rewrite using equality of propositions **********************************)

(***) Axiom iff_eq : (P,Q:Prop)(P -> Q) -> (Q -> P) -> P==Q.


(*** for convenience we give an axiom fixing the realizations
of elements of nat as being the standard finite ordinals ***)

(***) Axiom nat_realization_O : (x:E)~(inc x (R O)). 
(***) Axiom nat_realization_S : (n:nat; x:E)
(inc x (R (S n))) == ((inc x (R n)) \/ (x == (R n))). 




(********* END OF PARAMETERS AND AXIOMS *********************************************)

End Axioms.

Export Axioms.



Module Tactics1.
Tactic Definition ir := Intros.

Tactic Definition rw u := Rewrite u.
Tactic Definition rwi u h := Rewrite u in h.

Tactic Definition wr u := Rewrite <- u.
Tactic Definition wri u h := Rewrite <- u in h.

Tactic Definition ap h := Apply h.

Tactic Definition EasyAssumption := 
Match Context With 
[id1 : (?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8) |- (?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8)] -> Exact id1 |
[id1 : (?1 ?2 ?3 ?4 ?5 ?6 ?7) |- (?1 ?2 ?3 ?4 ?5 ?6 ?7)] -> Exact id1 |
[id1 : (?1 ?2 ?3 ?4 ?5 ?6) |- (?1 ?2 ?3 ?4 ?5 ?6)] -> Exact id1 |
[id1 : (?1 ?2 ?3 ?4 ?5) |- (?1 ?2 ?3 ?4 ?5)] -> Exact id1 |
[id1 : (?1 ?2 ?3 ?4) |- (?1 ?2 ?3 ?4)] -> Exact id1 |
[id1 : (?1 ?2 ?3) |- (?1 ?2 ?3)] -> Exact id1 |
[id1 : (?1 ?2) |- (?1 ?2)] -> Exact id1 |
[id1 : ?1 |- ?2] -> ap id1 |
_ -> Fail.

Tactic Definition am := Solve [EasyAssumption | Assumption].




Tactic Definition au := First [Solve [EasyAssumption] |Auto].
Tactic Definition eau := EAuto. 
Tactic Definition tv := Trivial.
Tactic Definition sy := Symmetry.

Tactic Definition uf u := Unfold u.
Tactic Definition ufi u h := Unfold u in h.

Tactic Definition nin h := NewInduction h.




Tactic Definition CompareTac a b := 
Assert toclear : a == a; [Exact (refl_eqT ? b) |Clear toclear].

Tactic Definition UnfoldHead1 h := 
Match h With
[(?1 ?2)] -> Unfold ?1 in h
|
_ -> Fail.

(*** we don't actually want to unfold certain things ***)
Tactic Definition Good_Unfold g h := 
Match g With 
[inc] ->  Fail
|
_ -> Unfold g in h.

Tactic Definition Unfold_Head_R g h := 
Match g With 
[(?1 ? ? ? ? ? ? ? ? ? ?)] -> Good_Unfold ?1  h |
[(?1 ? ? ? ? ? ? ? ? ? )] -> Good_Unfold ?1  h |
[(?1 ? ? ? ? ? ? ? ?)] -> Good_Unfold ?1  h |
[(?1 ? ? ? ? ? ? ?)] -> Good_Unfold ?1  h |
[(?1 ? ? ? ? ? ?)] -> Good_Unfold ?1  h |
[(?1 ? ? ? ? ?)] -> Good_Unfold ?1  h |
[(?1 ? ? ? ?)] -> Good_Unfold ?1  h |
[(?1 ? ? ?)] -> Good_Unfold ?1  h |
[(?1 ? ?)] -> Good_Unfold ?1  h |
[(?1 ?)] -> Good_Unfold ?1  h |
[?1] -> Good_Unfold ?1  h .


Tactic Definition Unfold_Head h := 
Match Context With 
[id1 : ?1 |- ? ] -> CompareTac id1 h; Unfold_Head_R ?1 h
|
_-> Fail.

Recursive Tactic Definition Exploit h := 
Match Context With 
[id1 : ?1 |- ? ] -> CompareTac id1 h; 
Assert ?1; [am | Unfold_Head h;  Exploit h]
|
_-> Idtac.

Tactic Definition xlt h := Exploit h.

Definition DONE := [A:Type; a:A]a.
Definition TODO := [A:Type; a:A]a.

Recursive Tactic Definition TodoAll := 
Match Context With 
[id1 : ?1 |- ? ] -> 
(Match ?1 With [(TODO ?)] -> Fail | _-> 
Change (TODO ?1)  in id1; TodoAll)
| _-> Idtac.

Definition CheckProp := [P:Prop]P.

Tactic Definition CheckPropTac P :=
Assert toclear: (CheckProp P); [am | Clear toclear].




Syntactic Definition E1 := E -> E.
Syntactic Definition E2 := E -> E1.
Syntactic Definition E3 := E -> E2.
Syntactic Definition E4 := E -> E3.
Syntactic Definition E5 := E -> E4.
Syntactic Definition E6 := E -> E5.
(** thus for example E3 = E -> E -> E -> E **)

Syntactic Definition EP := E -> Prop.
Syntactic Definition E2P := E -> EP.
Syntactic Definition E3P := E -> E2P.
Syntactic Definition E4P := E -> E3P.


Definition A := and.


Recursive Tactic Definition Deconj :=
Match Context With
[|- (A ?  ?)] -> Unfold A; ap conj; [Deconj |Deconj]
|
[|- (and ?  ?)] -> ap conj; [Deconj |Deconj]
|
[|-  ? /\ ?] -> ap conj; [Deconj |Deconj]

|
[|- ?]  -> au.

Recursive Tactic Definition EasyDeconj :=
Match Context With
[|- (A ?  ?)] -> Unfold A; ap conj; [EasyDeconj |EasyDeconj]
|
[|- (and ?  ?)] -> ap conj; [EasyDeconj |EasyDeconj]
|
[|-  ? /\ ?] -> ap conj; [EasyDeconj |EasyDeconj]

|
[|- ?]  -> Idtac.




Recursive Tactic Definition Expand := 
Match Context With 
[id1 : (A ?1 ?2) |- ?] -> (Unfold A in id1); nin id1; Expand
|
[id1 : (and ?1 ?2) |- ?] -> nin id1; Expand
|
[id1 : (?1 /\ ?2) |- ?] -> nin id1; Expand
|
[|- ?] -> Deconj.



(*** we write a tactic which is like Pose but which is anonymous ***)
Tactic Definition Remind u := 
Pose recalx := u;
Match Context With
[recalx : ?1 |- ? ] -> (Assert ?1; [Exact recalx | Clear recalx]).




Recursive Tactic Definition EasyExpand := 
Match Context With 
[id1 : (A ?1 ?2) |- ?] -> (Unfold A in id1); nin id1; EasyExpand
|
[id1 : (and ?1 ?2) |- ?] -> nin id1; EasyExpand
|
[id1 : (?1 /\ ?2) |- ?] -> nin id1; EasyExpand
|
[|- ?] -> EasyDeconj.


Tactic Definition ee := EasyExpand.

Tactic Definition xd := Expand.




Recursive Tactic Definition PreExplode n := 
Match n With 
[O] -> Idtac
|
[(S ?1)] -> 
(Match Context With
[id1 : ?2 |- ? ] -> CheckPropTac ?2; 
(Match ?2 With [(DONE ?3)] -> Fail | _ ->
Assert (DONE ?2); [Unfold DONE; am | Unfold_Head id1; EasyExpand; PreExplode ?1] )
| _-> Idtac
).

Recursive Tactic Definition ClearDone := 
Match Context With
[id1 : (DONE ?1) |- ? ] -> Unfold DONE in id1; ClearDone
|
_-> Idtac.



Tactic Definition Exp := PreExplode '(5); ClearDone.
Tactic Definition Expl := PreExplode '(10); ClearDone. 
Tactic Definition Explode := PreExplode '(100); ClearDone.



Recursive Tactic Definition CleanUp := 
Match Context With 
[id1 : ?1; id2 : ?1 |- ? ] -> 
CheckPropTac ?1; Clear id2; CleanUp
|
_-> Idtac.

Tactic Definition xde := Explode.
Tactic Definition cx := Explode; CleanUp.

(***** we would like a general Cycle construction (can we parametrize tactics over tactics???) ***)


Tactic Definition sh x:= 
First [ap nonemptyT_intro; Exact x
|
Apply exT_intro with x
|
Apply exists_intro with x
|
Apply nonempty_intro with x].


Lemma seq_deconj : (P,Q:Prop)P -> (P -> Q) -> (A P Q). 
ir. xd. Save. 

Recursive Tactic  Definition dj :=
Match Context With 
[|- (A ?1 ?2)] -> ap seq_deconj; ir; dj
|
_ -> Idtac. 



Recursive Tactic Definition MiddleDeconj :=
Match Context With
[|- (A ?  ?)] -> Unfold A; ap conj; [MiddleDeconj |MiddleDeconj]
|
[|- (and ?  ?)] -> ap conj; [MiddleDeconj |MiddleDeconj]
|
[|-  ? /\ ?] -> ap conj; [MiddleDeconj |MiddleDeconj]

|
[|- ?]  -> First[Solve[Trivial | EasyAssumption |sy; EasyAssumption] | Idtac].



Recursive Tactic Definition MiddleExpand := 
Match Context With 
[id1 : (A ?1 ?2) |- ?] -> (Unfold A in id1); nin id1; MiddleExpand 
|
[id1 : (and ?1 ?2) |- ?] -> nin id1; MiddleExpand 
|
[id1 : (?1 /\ ?2) |- ?] -> nin id1; MiddleExpand 
|
[|- ?] -> MiddleDeconj.

Tactic Definition xe := MiddleExpand.

Definition type_of := [T:Type; t:T]T.

Tactic Definition Copy a :=
Assert (type_of a); [Exact a|
Match Context With
[id1 : (type_of ?) |- ?] -> (ufi type_of id1)].

Tactic Definition ufk a b := Copy b; ufi a b.

Tactic Definition uh a := Red in a.
(*** replaces Unfold_Head a. as mentionned by Hugo ***)

Tactic Definition uhg := Red. 
(*** Match Context With 
[|-(?1 ? ? ? ? ? ? ? ? ? ?)] -> Unfold ?1 |
[|-(?1 ? ? ? ? ? ? ? ? ?)] -> Unfold ?1 |
[|-(?1 ? ? ? ? ? ? ? ?)] -> Unfold ?1 |
[|-(?1 ? ? ? ? ? ? ?)] -> Unfold ?1 |
[|-(?1 ? ? ? ? ? ?)] -> Unfold ?1 |
[|-(?1 ? ? ? ? ?)] -> Unfold ?1 |
[|-(?1 ? ? ? ?)] -> Unfold ?1 |
[|-(?1 ? ? ?)] -> Unfold ?1 |
[|-(?1 ? ?)] -> Unfold ?1 |
[|-(?1 ?)] -> Unfold ?1 |
_-> Idtac.
***)

End Tactics1.
Export Tactics1.




Module Constructions.

Definition neq := [x,y:E]~(x == y).




Lemma sub_trans : (a,b,c:E)(sub a b) -> (sub b c) -> (sub a c).
Unfold sub. eau. Save. 



Lemma inc_nonempty : (x,y:E)(inc x y) -> (nonemptyT y).
ir. Unfold inc in H. nin H. ap nonemptyT_intro. am.
Save.

Lemma R_inc : (x:E; a:x)(inc (R a) x).
ir. Unfold inc. EApply exT_intro with a. tv.
Save.

Definition B := [x,y:E; hyp : (inc x y)]
(chooseT [a:y](R a) == x (inc_nonempty hyp)).

Lemma B_eq : (x,y:E; hyp : (inc x y))(R (B hyp)) == x.
ir. Unfold B.
Pose (chooseT_pr 2![a:y](R a) == x).
ap e. am.
Save.

Definition empty := [x:E](y:E)~(inc y x). 

Lemma nonemptyT_not_empty : (x:E)(nonemptyT x) -> ~(empty x).
ir. nin H. Unfold not. Unfold empty. ir. Unfold not in H.
Apply H with (R X). ap R_inc. Save. 



Lemma not_empty_nonemptyT : (x:E)~(empty x) -> (nonemptyT x).
ir. ap excluded_middle. Unfold  not. ir. Unfold not in H. 
ap H. Unfold empty. Unfold not. ir. ap H0. ap nonemptyT_intro. 
Exact (B H1). Save. 



Inductive emptyset : E := .

Lemma emptyset_empty : (x:E)~(inc x emptyset).
Unfold not. ir.
Pose (B H).
Elim e.
Save.


Definition strict_sub := [a,b:E]
(A (neq a b)
   (sub a b)
).

Lemma strict_sub_trans1 : (a,b,c:E)(strict_sub a b) -> (sub b c) -> 
(strict_sub a c).
Unfold strict_sub. Unfold neq. Unfold not. ir. 
xd. ir. ap H. ap extensionality. 
am. Rewrite H2. am. xd. 
Apply sub_trans with b; au. Save. 



Lemma strict_sub_trans2 : (a,b,c:E)(sub a b) -> (strict_sub b c) -> 
(strict_sub a c).
Unfold strict_sub. Unfold neq. Unfold not. ir. 
xd. ir. ap H0. ap extensionality. 
am. Rewrite <- H2. am. xd. 
Apply sub_trans with b; au. Save. 





Definition exists_unique := [p:E->Prop]
(A (exists p)
   (x,y:E)(p x) -> (p y) -> x == y
).

Lemma exT_exists : (p:E-> Prop)(exT ? [x:E](p x)) -> (exists p).
ir.
nin H.
Pose exists_intro.
eau.
Save.




Lemma p_or_not_p : (P:Prop)P \/ (not P).
ir.
EApply excluded_middle.
Unfold not.
ir.
Assert P; ap excluded_middle; Unfold not; au.
Save.




Definition choose : (E -> Prop) -> E.
ir.
EApply chooseT.
am.
EApply nonemptyT_intro.
Exact Prop.
Defined.


Lemma choose_pr : (p:E -> Prop)(exists p) -> (p (choose p)).
ir.
Unfold choose.
EApply chooseT_pr.
nin H.
Apply exT_intro with x.
am.
Save.


Definition rep := [x:E](choose [y:E](inc y x)). 

Lemma nonempty_rep : (x:E)(nonempty x) -> (inc (rep x) x). 
ir. nin H. Unfold rep. ap choose_pr.
Apply exists_intro with y. 
am. Save. 





Definition by_cases_pr:= [T:Type; P:Prop; a:P -> T; b:(not P) -> T; x:T]
(A (p:P)(a p) == x
   (q:(not P))(b q) == x
).

Lemma by_cases_exists : (T:Type; P:Prop; a:P -> T; b:(not P) -> T)
(exT ? [x:T](by_cases_pr a b x)).
ir. Assert (P \/ (not P)). ap p_or_not_p. nin H.
EApply exT_intro with (a H). Unfold by_cases_pr. xd.
ir. Assert H==p. ap proof_irrelevance. Rewrite H0. tv.
ir. Pose (q H). Elim f.
EApply exT_intro with (b H). Unfold by_cases_pr. xd.
ir. Pose (H p). Elim f.
ir. Assert H == q. ap proof_irrelevance. Rewrite H0. tv.
Save.

Lemma by_cases_nonempty : (T:Type; P:Prop; a:P -> T; b:(not P) -> T)
(nonemptyT T).
ir.
ir. Assert (P \/ (not P)). ap p_or_not_p. nin H.
EApply nonemptyT_intro. Exact (a H).
EApply nonemptyT_intro. Exact (b H).
Save.



Definition by_cases := [T:Type; P:Prop; a:P -> T; b:(not P) -> T]
(chooseT [x:T](by_cases_pr a b x) (by_cases_nonempty a b)).


Lemma by_cases_property : (T:Type; P:Prop; a:P -> T; b:(not P) -> T)
(by_cases_pr a b (by_cases a b)).
ir.
Remind '(by_cases_exists a b).
Remind '(by_cases_nonempty a b).
Remind '(chooseT_pr H0 H).
Unfold by_cases.
Assert (by_cases_nonempty a b) == H0.
ap proof_irrelevance.
Rewrite H2.
am.
Save.

Lemma by_cases_unique : (T:Type; P:Prop; a:P -> T; b:(not P) -> T; x:T)
(by_cases_pr a b x) -> (by_cases a b) == x.
ir.
Remind '(by_cases_property a b).
ir. Assert (P \/ (not P)). ap p_or_not_p. nin H1.
Unfold by_cases_pr in H.  Unfold by_cases_pr in H0.  xd.
Transitivity (a H1). sy. au. au.
Unfold by_cases_pr in H.  Unfold by_cases_pr in H0.  xd.
Transitivity (b H1). sy. au. au.
Save.


Lemma by_cases_if  : (T:Type; P:Prop; a:P -> T; b:(not P) -> T; p:P)
(by_cases a b) == (a p).
ir. EApply by_cases_unique.
Unfold by_cases_pr. xd.
ir. Assert p == p0. ap proof_irrelevance. Rewrite H. tv.
ir. Remind '(q p). Elim H.
Save.



Lemma by_cases_if_not :  (T:Type; P:Prop; a:P -> T; b:(not P) -> T; q : (not P))
(by_cases a b) == (b q).
ir. EApply by_cases_unique.
Unfold by_cases_pr. xd.
ir.
Remind '(q p). Elim H.
ir. Assert q == q0. ap proof_irrelevance. Rewrite H. tv.
Save.



Lemma exists_proof : (p:E->Prop)(not (x:E)(not (p x))) -> (exists p).
ir. Unfold not in H. EApply excluded_middle. Unfold not.
ir. ap H. ir. ap H0. EApply exists_intro with x.
am. 
Save.

Lemma not_exists_pr : (p:E-> Prop)(not (exists p)) <-> ((x:E)(not (p x))).
ir. Unfold iff. ap conj. ir. Unfold not. Unfold not in H.
ir. ap H. Apply exists_intro with x. am.
  ir. Unfold not. Unfold not in H. ir. nin H0.
Apply H with x. am. 
Save. 

Definition Yy :(P:Prop; f:P-> E)E -> E.
Intros P f x. Apply by_cases with P. Exact f.
ir. Exact x. Defined. 

Lemma Yy_if : (P:Prop; hyp : P; f:P-> E; x,z:E)(f hyp) == z ->
(Yy f x) == z. 
ir. Unfold Yy. Pose b := [p:~P]x. 
Rewrite <- H. ap by_cases_if. Save. 

Lemma Yy_if_not : (P:Prop; hyp : ~P; f:P-> E; x,z:E)x == z ->
(Yy f x) == z. 
ir. Unfold Yy. Pose b := [p:~P]x.
Transitivity (b hyp). ap by_cases_if_not. tv. 
Save.

Definition Y : Prop -> E -> E -> E.
Intros P x y.
EApply by_cases with P.
ir. Exact x.
ir. Exact y.
Defined.

Lemma Y_if : (P:Prop; hyp : P; x,y,z:E) x == z -> (Y P x y) == z.
ir. Unfold Y. Pose a:= [p:P]x. Pose b := [p:~P]y.
Transitivity (a hyp). ap by_cases_if. Transitivity x. 
tv.
am. Save.

Lemma Y_if_not : (P:Prop; hyp : (not P); x,y,z:E) y == z -> 
(Y P x z) == y.
ir. Unfold Y. Pose a:= [p:P]x. Pose b := [p:~P]z.
Transitivity (b hyp).  ap by_cases_if_not. Rewrite H. tv.
Save.

Record Rec [x:E; f:x -> E] : E := join {
head : x;
tail : (f head)
}.
Implicits join [1 2].

Definition Z : E -> (E -> Prop) -> E.
Intros x p.
Pose (Rec [a:x](p (R a))).
Exact (IM [t:T](R (head t))).
Defined.

Lemma Z_inc : (x:E; p: E -> Prop; y:E)(inc y x) -> (p y) -> (inc y (Z x p)).
ir. Unfold Z. EApply IM_inc. Unfold inc in H. nin H.
Assert (p (R x0)). Rewrite H. am.
Pose (join 2![a:x](p (R a)) x0 H1). Apply exT_intro with r. tv.
Save.

Lemma Z_sub : (x:E; p: E -> Prop)(sub (Z x p) x).
ir. Unfold sub. ir. Pose (IM_exists H).
nin e. Rewrite <- H0. ap R_inc.
Save.

Lemma Z_pr : (x:E; p: E-> Prop; y:E)(inc y (Z x p)) -> (p y).
ir. Unfold inc in H. nin H. Unfold Z in x0.
Pose (R_inc x0). Pose (IM_exists i). 
nin e. Pose (tail x1).
Rewrite H0 in p0. Rewrite <- H. am.
Save.

Lemma Z_all : (x:E; p: E-> Prop; y:E)(inc y (Z x p)) -> 
(A (inc y x) (p y)).
ir. xd. Assert (sub (Z x p) x). ap Z_sub.
ap H0; am.
Pose _:=(Z_pr H); au.
Save.

Tactic Definition Ztac := 
Match Context With 
[id1 : (inc ?1 (Z ? ?)) |- ? ] -> Pose (Z_all id1); xd
|
[|- (inc ? (Z ? ?))] -> ap Z_inc; au
|
_ -> Idtac.


Definition X := [x:E; f: x -> E; y:E]
(Yy [hyp : (inc y x)](f (B hyp)) emptyset). 

Lemma X_eq : (x:E; f: x -> E; y,z: E)
(exT ? [a:x](A (R a) == y (f a) == z)) -> (X f y) == z. 
ir. nin H. xd. Unfold X. 
Assert (inc y x). Rewrite <- H. ap R_inc. 
Apply Yy_if with H1. Assert (B H1) == x0.  
ap R_inj. Rewrite B_eq. au. Rewrite H2. am.
Save. 

Lemma X_rewrite : (x:E; f: x -> E; a:x)
(X f (R a)) == (f a). 
ir. 
ap X_eq. Apply exT_intro with a. xd.
Save. 


Definition cut := [x:E; p: x -> Prop]
(Z x [y:E](hyp : (inc y x))(p (B hyp))). 

Lemma cut_sub : (x:E; p: x -> Prop)(sub (cut p) x). 
ir. Unfold cut. ap Z_sub. Save. 


Definition cut_to := [x:E; p: x -> Prop; y: (cut p)]
(B ((cut_sub 2!p) ? (R_inc y))). 

Lemma cut_to_R_eq : (x:E; p: x -> Prop; y: (cut p))
(R (cut_to y)) == (R y). 
ir. Unfold cut_to. Rewrite B_eq. tv. Save. 



Lemma cut_pr : (x:E; p: x -> Prop; y:(cut p))(p (cut_to y)).
ir. Unfold cut_to. Unfold cut in y. 
LetTac k :=  [y:E](hyp:(inc y x))(p (B hyp)). 
Pose (R_inc y). 
Ztac.
Save. 


Lemma cut_inc : (x:E; p: x -> Prop; y:x)(p y) -> 
(inc (R y) (cut p)). 
ir. Unfold cut. ap Z_inc. ap R_inc. ir. 
Assert (B hyp) == y. ap R_inj. ap B_eq. Rewrite H0. 
am. Save. 





Definition IM_lift : (a:E; f: a-> E)(IM f) -> a. 
ir. Assert (exT ? [x:a](f x) == (R X0)). ap IM_exists. 
ap R_inc. Assert (nonemptyT a). nin H. 
ap nonemptyT_intro; am. Exact (chooseT [x:a](f x) == (R X0) H0). 
Defined. 

Lemma IM_lift_pr : (a:E; f: a-> E; x:(IM f))
(f (IM_lift x)) == (R x). 
ir. Assert (exT ? [y:a](f y) == (R x)). ap IM_exists. 
ap R_inc.  uf IM_lift. LetTac K:= (exT_ind a [x0:a](f x0)==(R x) 
(nonemptyT a)
      [x0:a; _:((f x0)==(R x))](nonemptyT_intro x0) 
(IM_exists (R_inc x))). 
Pose (chooseT_pr K H). am. 
Save. 



End Constructions.

Export Constructions.

Module Little.



Inductive one_point : E := point : one_point.

Definition singleton := [x:E](IM [p:one_point]x).

Lemma singleton_inc : (x:E)(inc x (singleton x)).
ir. Unfold singleton. ap IM_inc.
Apply exT_intro with point. tv. Save.

Lemma singleton_eq : (x,y:E)(inc y (singleton x)) -> y == x.
ir. Pose (IM_exists H). nin e.
sy. tv. Save.


Lemma singleton_inj : (x,y: E)(singleton x) == (singleton y) -> x == y. 
ir. Assert (inc x (singleton y)). Rewrite <- H.
ap singleton_inc.
ap singleton_eq. am. Save.









Inductive two_points : E := 
first : two_points | second : two_points.

Definition doubleton_map : (x,y:E)two_points -> E.
Intros x y t. nin t. Exact x. Exact y. Defined.

Definition doubleton := [x,y:E](IM (doubleton_map x y)).

Lemma doubleton_first : (x,y:E)(inc x (doubleton x y)).
ir. Unfold doubleton. ap IM_inc. Apply exT_intro with first.
tv. Save.


Lemma doubleton_second : (x,y:E)(inc y (doubleton x y)).
ir. Unfold doubleton. ap IM_inc. Apply exT_intro with second.
tv. Save.



Lemma doubleton_or : (x,y,z:E)(inc z (doubleton x y)) -> (z == x) \/ (z == y).
ir. Pose (IM_exists H). nin e. nin x0.
Compute in H0.
Intuition.
Compute in H0. Intuition. Save.   


Lemma doubleton_inj : (x,y,z,w:E)(doubleton x y) == (doubleton z w) -> 
(A x == z y == w) \/ (A x == w y == z). 
ir. Assert (inc x (doubleton z w)). Rewrite <- H. ap doubleton_first. 
Pose (doubleton_or H0). Assert (inc y (doubleton z w)). 
Rewrite <- H. 
ap doubleton_second. Pose (doubleton_or H1). nin o.
nin o0. Assert (inc w (doubleton x y)). Rewrite H. 
ap doubleton_second. Pose (doubleton_or H4). nin o. 
ap or_introl. xd. Rewrite H5. Rewrite H2. am.
ap or_introl. xd. 
ap or_introl. xd. 
nin o0.
ap or_intror. xd. 
Assert (inc z (doubleton x y)). Rewrite H. ap doubleton_first. 
Pose (doubleton_or H4). nin o. ap or_introl. xd. 
ap or_introl. xd. Rewrite H5. Rewrite H3. 
am. Save.



End Little.

Module Complement. 

Definition complement := [a,b:E](Z a [x:E]~(inc x b)).

Lemma inc_complement : (a,b,x:E)(inc x (complement a b)) ==
(A (inc x a) ~(inc x b)).
ir.
ap iff_eq; ir.
ufi complement H; Ztac.

uf complement; ap Z_inc.
xd.

xd.
Save. 


Lemma use_complement : (a,b,x:E)(inc x a) -> ~(inc x (complement a b)) -> (inc x b).
ir.
ap excluded_middle.
uf not; ir.
ap H0.
uf complement; ap Z_inc.
am.

am.
Save. 

End Complement.
Export Complement.

Module Pair.

Export Little.

Definition pair := [x,y:E]
(doubleton (singleton x) (doubleton emptyset (singleton y))).

Definition is_pair := [u:E](exists [x:E](exists [y:E]u== (pair x y))).

Lemma lem1 : (x,y,z,w:E)(pair x y) == (pair z w) -> x == z.
ir. Assert (inc (singleton x) (pair z w)). Rewrite <- H.
Unfold pair. ap doubleton_first. Unfold pair in H0. Pose (doubleton_or H0). 
nin o. ap singleton_inj. am. Assert (inc emptyset (singleton x)).
Rewrite H1. ap doubleton_first. Assert (inc (singleton w) (singleton x)). 
Rewrite H1. ap doubleton_second. Assert emptyset == x. ap singleton_eq. am.
Assert (singleton w) == x. ap singleton_eq. am. Assert (inc w emptyset).
Rewrite H4. Rewrite <- H5. ap singleton_inc. Pose (emptyset_empty H6). 
Elim f. Save. 


Lemma lem2 : (x,y,z,w:E)(pair x y) == (pair z w) -> y == w.
ir. Assert (inc (doubleton emptyset (singleton y)) (pair z w)). 
Rewrite <- H. Unfold pair. ap doubleton_second. Unfold pair in H0.
Pose (doubleton_or H0). nin o. Assert (inc emptyset (singleton z)).
Rewrite <- H1. ap doubleton_first. Assert (inc (singleton y) (singleton z)).
Rewrite <- H1. ap doubleton_second. Pose (singleton_eq H2).
Pose (singleton_eq H3). Assert (inc y emptyset). Rewrite e. Rewrite <- e0.
ap singleton_inc. Pose (emptyset_empty H4). Elim f. 
Assert (inc (singleton y) (doubleton emptyset (singleton w))). 
Rewrite <- H1. ap doubleton_second. Pose (doubleton_or H2). 
nin o. Assert (inc y emptyset). Rewrite<- H3. ap singleton_inc. 
Pose (emptyset_empty H4). Elim f. ap singleton_inj. am. Save. 




Definition pr1 := [u:E](choose [x:E](exists [y:E]u== (pair x y))).
Definition pr2 := [u:E](choose [y:E](exists [x:E]u == (pair x y))).

Syntactic Definition J := pair.
Syntactic Definition P := pr1.
Syntactic Definition Q := pr2. 


Definition pair_recovers := [u:E](pair (pr1 u) (pr2 u)) == u.

Lemma pair_recov : (u:E)(is_pair u) -> (pair_recovers u).
ir. Unfold is_pair in H. Unfold pair_recovers. 
Pose (choose_pr H). Assert (exists [y:E](exists [x:E]
(u == (pair x y)))).
nin e. Apply exists_intro with x. Apply
exists_intro with (pr1 u). am. Pose (choose_pr H0).
nin e. nin e0. Assert u == (pair (pr1 u) x). 
am. Assert u == (pair x0 (pr2 u)). am. 
Assert (pair (pr1 u) x) == (pair x0 (pr2 u)). Rewrite <- H3.
am. Pose (lem1 H5). Rewrite e. sy. am. 
Save. 

Lemma pair_is_pair : (x,y:E)(is_pair (pair x y)). 
ir. Unfold is_pair. Apply exists_intro with x.
Apply exists_intro with y. tv. Save. 


Lemma pr1_pair : (x,y:E)(pr1 (pair x y)) == x.
ir. LetTac u := (pair x y). Assert (is_pair u). 
Unfold u. ap pair_is_pair. Pose (pair_recov H). 
Unfold pair_recovers in (Type of p). Unfold u in 
(Type of p). Pose (lem1 p). am. Save. 

 

Lemma pr2_pair : (x,y:E)(pr2 (pair x y)) == y.
ir. LetTac u := (pair x y). Assert (is_pair u). 
Unfold u. ap pair_is_pair. Pose (pair_recov H). 
Unfold pair_recovers in (Type of p). Unfold u in 
(Type of p). Pose (lem2 p). am. Save. 




Definition V := [x,f:E](choose [y:E](inc (pair x y) f)).

Lemma V_inc : (x,z,f:E)(exists [y:E](inc (pair x y) f)) -> 
z == (V x f) ->
(inc (pair x z) f). 
ir. Pose (choose_pr H). Rewrite H0. am. Save. 




End Pair.
Export Pair.

Module Image. 

Definition create := [x:E; f: E1](IM [a:x](f (R a))). 

Lemma  incl : (x:E; f:E -> E; a:E)(inc a x) -> 
(inc (f a) (create x f)).
ir. Unfold create. ap IM_inc. 
Apply exT_intro with (B H). Pose (B_eq H). Rewrite e. 
tv. Save. 


Lemma show_inc : (x:E; f:E -> E; z:E)
(exists [a:E](A (inc a x) (f a) == z)) -> (inc z (create x f)).
ir. nin H. xd. Rewrite <- H0. 
ap incl. am. Save. 

Lemma ex : (x:E; f:E-> E; a:E)(inc a (create x f)) ->
(exists [b:E](A (inc b x) (f b) == a)).
ir. Pose (IM_exists H). nin e. Apply exists_intro
 with (R x0). xd. Unfold inc. Apply exT_intro with x0. 
tv. Save. 





End Image.

Module Powerset. 

Definition powerset := [x:E](IM [p:x-> Prop](cut p)).


Lemma powerset_inc : (x,y:E)(sub x y) -> (inc x (powerset y)). 
ir. Unfold powerset. ap IM_inc. Apply exT_intro with
[b:y](inc (R b) x). ap extensionality. Unfold sub. ir. 
Pose (B H0). Pose (B_eq H0). Pose (cut_pr c). Assert 
x0 == (R (cut_to c)). Transitivity (R c). Unfold c. 
au. sy. ap cut_to_R_eq. Rewrite H1. am. 
Unfold sub. ir. Pose (B H0). Pose (B_eq H0). 
Rewrite <- e. Unfold cut. ap Z_inc. ap H. Rewrite e. 
am. ir. Pose (B_eq hyp). Rewrite e0. 
Rewrite e. am. Save. 


Lemma powerset_sub : (x,y:E)(inc x (powerset y)) -> (sub x y).
ir. Unfold powerset in H. Pose (IM_exists H). nin e. 
Rewrite <- H0. ap cut_sub. Save. 

End Powerset. 
Export Powerset. 

Module Union. 

Record  Integral [x:E] : E := {
param : x;
elt : (R param)
}.

Definition union := [x:E](IM [i:(Integral x)](R (!elt x i))).




Lemma union_inc : (x,y,a:E)(inc x y) -> (inc y a) -> 
(inc x (union a)).
ir. 
Pose (B H0). Assert (R a0) == y. Unfold a0. ap B_eq. 
Assert (inc x (R a0)). Rewrite H1. am. 
Pose (B H2). Pose (!Build_Integral a a0 r). Unfold union.
ap IM_inc. Apply exT_intro with i. Change (R r) == x. 
Unfold r. ap B_eq. Save. 



Lemma union_exists : (x,a:E)(inc x (union a)) -> 
(exists [y:E](A (inc x y) (inc y a))).
ir. Unfold union in H. Pose (IM_exists H). 
nin e. Apply exists_intro with (R (param x0)). 
xd. Rewrite <- H0. ap R_inc. ap R_inc. Save. 

Definition union2 := [x,y:E](union (doubleton x y)). 


Lemma union2_or : (x,y,a:E)(inc a (union2 x y)) -> 
((inc a x) \/ (inc a y)).
ir. Unfold union2 in H. Pose (union_exists H). 
nin e. xd. Pose (doubleton_or H1). 
nin o. Rewrite H2 in H0. Intuition. 
Rewrite H2 in H0; Intuition. Save. 


Lemma union2_first : (x,y,a:E)(inc a x)-> (inc a (union2 x y)).
ir. Unfold union2. Apply union_inc with x. am.
ap doubleton_first. Save. 

Lemma union2_second : (x,y,a:E)(inc a y)-> (inc a (union2 x y)).
ir. Unfold union2. Apply union_inc with y. am.
ap doubleton_second. Save. 


End Union. 

Export Union. 

Module Intersection. 


Definition intersection := [x:E](Z (rep x) [y:E]
(z:E)(inc z x) -> (inc y z)). 

Lemma intersection_inc : (x,a:E)(nonempty x) -> 
((y:E)(inc y x) -> (inc a y)) -> (inc a (intersection x)). 
ir. Unfold intersection. ap Z_inc. 
Pose (nonempty_rep H). ap H0. am. am. 
Save. 

Lemma intersection_forall : (x,a,y:E) 
(inc a (intersection x)) -> (inc y x) -> (inc a y). 
ir. Unfold intersection in H. 
Ztac. Save.

Lemma intersection_sub : (x,y:E)
(inc y x) -> (sub (intersection x) y).
ir.
Unfold sub.
ir.
Apply intersection_forall with x; au.
Save.


Definition intersection2 : E -> E -> E 
:= [x,y:E](intersection (doubleton x y)).

Lemma intersection2_inc : (x,y,a:E)(inc a x) -> 
(inc a y) ->(inc a (intersection2 x y)).
ir.
Unfold intersection2.
ap intersection_inc.
Apply nonempty_intro with x.
ap doubleton_first.
ir.
Remind '(doubleton_or H1).
nin H2.
Rewrite H2.
am.
Rewrite H2.
am.
Save.

Lemma intersection2_first : (x,y,a:E)(inc a (intersection2 x y)) -> (inc a x).
ir.
Unfold intersection2 in H.
EApply intersection_forall with (doubleton x y).
am.
ap doubleton_first.
Save.




Lemma intersection2_second : (x,y,a:E)(inc a (intersection2 x y)) -> (inc a y).
ir.
Unfold intersection2 in H.
EApply intersection_forall with (doubleton x y).
am.
ap doubleton_second.
Save.


Lemma intersection_use_inc : (x,y:E)(inc y (intersection x)) ->
((z:E)(inc z x) -> (inc y z)).
ir. Apply intersection_forall with x; am.
Save. 


End Intersection.

Export Intersection. 





Module Transposition.

Definition create := [i,j,a:E]
(Y (a == i) j
(Y (a == j) i
   a
)).



Lemma not_i_not_j : (i,j,a:E)(not a==i) -> (not a==j) -> (create i j a) == a.
ir. Unfold create. Apply (Y_if_not H). sy. 
Apply (Y_if_not H0). tv. 
Save.

Lemma i_j_j_i : (i,j,a:E)(create i j a) == (create j i a).
ir. Unfold create. Apply by_cases with a==i. ir. 
ap '(Y_if H). sy. Apply by_cases with a == j. 
ir. ap '(Y_if H0). Rewrite <- H. am. 
ir. ap '(Y_if_not H0). sy. ap '(Y_if H). 
tv. ir. ap '(Y_if_not H). Apply by_cases with a== j. 
ir. ap '(Y_if H0). sy. ap '(Y_if H0). 
tv. 
ir. ap '(Y_if_not H0). ap '(Y_if_not H0). 
ap '(Y_if_not H). tv. Save. 


Lemma i_j_i : (i,j : E)(create i j i) == j.
ir. Unfold create. Assert i==i; tv. ap '(Y_if H). 
tv. 
Save.

Lemma i_j_j : (i,j : E)(create i j j) == i.
ir. Rewrite i_j_j_i. ap i_j_i. Save. 




Lemma i_i_a : (i,a:E)(create i i a) == a.
ir. Apply by_cases with a == i. ir. Rewrite H. 
ap i_j_j. ir. Unfold create. ap '(Y_if_not H). 
sy. ap '(Y_if_not H). tv. 
Save.



Lemma surj : (i,j,a:E)(exists [b:E](create i j b) == a).
ir.
Apply by_cases with a==i.
ir. Apply exists_intro with j. Rewrite H. ap i_j_j. 
ir. Apply by_cases with a==j. ir. 
Apply exists_intro with i. Rewrite H0. ap i_j_i. 
ir. 
Apply exists_intro with a. ap not_i_not_j. 
am. am. 
Save.


Lemma involutive : (i,j,a:E)(create i j (create i j a)) == a. 
ir. Apply by_cases with a==i. ir. 
Rewrite H. Rewrite i_j_i. ap i_j_j. 
Apply by_cases with a==j. ir. Rewrite H. Rewrite i_j_j. 
ap i_j_i. ir. Pose (not_i_not_j H0 H). 
Rewrite e. am. Save. 

Lemma inj : (i,j,a,b:E)(create i j a) == (create i j b) -> a == b.
ir. Transitivity (create i j (create i j a)). 
sy; ap  involutive. Rewrite H. ap involutive. 
Save. 



End Transposition.


Module Function.

Definition axioms :=  [f:E] 
(A (x:E)(inc x f) -> (pair (pr1 x) (pr2 x)) == x
   (x,y:E)(inc x f) -> (inc y f) -> (pr1 x) == (pr1  y) -> x == y
).

Definition domain [f:E] := (Image.create f pr1).
Definition range [f:E] := (Image.create f pr2).

Definition defined := [f,x:E]
(A (axioms f)
   (inc x (domain f))
).


Lemma sub_axioms : (f,g:E)(axioms g) -> (sub f g) -> (axioms f).
ir. 
nin H. 
Unfold sub in H0. 
Unfold axioms; xd.
Save.

Lemma sub_domain : (f,g:E)(sub f g) -> (sub (domain f) (domain g)).
ir. 
Unfold sub. 
Unfold domain. 
Unfold sub in H.
ir. 
LetTac K := (Image.ex H0). 
nin K. 
nin H1.
Rewrite <- H2. 
ap Image.incl. 
au.
Save.

Lemma sub_range : (f,g:E)(sub f g) -> (sub (range f) (range g)).
ir. 
Unfold sub. 
Unfold range. 
Unfold sub in H. 
ir.
LetTac K:= (Image.ex H0). 
nin K. 
nin H1.
Rewrite <- H2. 
ap Image.incl. 
au.
Save.


Lemma range_inc : (f,z:E)(axioms f)-> (exists [y:E](A (inc y (domain f))
(V y f) == z)) -> (inc z (range f)). 
ir. nin H0. xd. Unfold range. 
ap Image.show_inc. Apply exists_intro with (pair x z).
xd. ap V_inc. 
Unfold domain in H0.
Pose (Image.ex H0). nin e; xd. 
Apply exists_intro with (pr2 x0). 
Rewrite <- H3. Unfold axioms in H. xd. 
Rewrite H. am. am. au. ap pr2_pair. 
Save. 




Lemma defined_lem : (f,x:E)(axioms f) -> (defined f x) -> 
(inc (pair x (V x f)) f).
ir.
Unfold axioms in H.
Unfold defined in H0.
xd.
Unfold domain in H1.
LetTac K := (Image.ex H1).
nin K.
nin H3.
Assert (exists [y:E](inc (pair x y) f)).
EApply exists_intro with (pr2 x0).
Rewrite <- H4.
Rewrite H.
am.
am.
LetTac K := (choose_pr H5).
am.
Save.

Lemma lem1 : (f,x:E)(axioms f) -> (inc x f) -> x == (pair (pr1 x) (V (pr1 x) f)).
ir.
Unfold axioms in H.
xd.
LetTac z := (pr1 x).
Assert (exists [y:E](inc (pair z y) f)).
Apply exists_intro with (pr2 x).
Unfold z.
Rewrite H.
am.
am.
LetTac K := (choose_pr H2).
Assert (inc (pair z (V z f)) f).
am.
ap H1.
am.
am.
Rewrite pr1_pair.
tv.
Save.

Lemma lem2 : (f,x:E)(axioms f) -> (inc x f) -> 
(inc (pr1 x) (domain f)). 
ir. Unfold domain. ap Image.incl. am. 
Save. 

Lemma pr2_V : (f,x:E)(axioms f) -> (inc x f) -> (pr2 x) == (V (pr1 x) f).
ir.
Pose (lem1 H H0).
LetTac a:=(pr1 x).
Rewrite -> e.
Rewrite -> pr2_pair.
tv.
Save.

Lemma range_ex : (f,y:E)(axioms f) -> (inc y (range f)) -> 
(exists [x:E](A (inc x (domain f)) (V x f) == y)). 
ir. Unfold range in H0. Pose (Image.ex H0);
nin e; xd. Assert (axioms f).
am. Unfold axioms in H; xd.
Pose (H x H1). LetTac a := (pr1 x). LetTac b := (pr2 x). 
Apply exists_intro with a. xd. Unfold a;
ap lem2; au. 
Assert x == (pair a (V a f)). Unfold a. ap lem1; au. 
Rewrite <- H2. Unfold b. Rewrite H5. 
sy; ap pr2_pair. Save. 

Lemma function_sub : (f,g:E)(axioms f) -> (axioms g) ->
((x:E)(defined f x) -> (defined g x)) ->
((x:E)(defined f x) -> (V x f) == (V x g)) ->
(sub f g).
ir.
Unfold sub.
ir.
LetTac K := (lem1 H H3).
Assert (defined f (pr1 x)).
Unfold defined; xd.
Unfold domain.
ap Image.incl.
am.
Assert (V (pr1 x) f) == (V (pr1 x) g).
ap H2.
am.
Rewrite K.
Assert (defined g (pr1 x)).
ap H1.
am.
Unfold defined in H6.
xd.
Unfold domain in H7.
LetTac K1 := (Image.ex H7).
nin K1.
nin H8.
Unfold axioms in H0.
LetTac K1 := (lem1 H6 H8).
Rewrite H9 in K1.
Rewrite H5.
Rewrite <- K1.
am.
Save.


Lemma function_extensionality : (f,g:E)(axioms f) -> (axioms g) ->
((x:E)(defined f x) -> (defined g x)) ->
((x:E)(defined g x) -> (defined f x)) ->
((x:E)(defined f x) -> (V x f) == (V x g)) ->
f == g.
ir.
ap extensionality.
ap function_sub; au.
ap function_sub; au.
ir.
sy.
ap H3.
ap H2.
am.
Save.


Definition inverse_image := [a,f:E]
(Z (domain f) [x:E](inc (V x f) a)). 


Lemma inverse_image_sub : (a,f:E)
(sub (inverse_image a f) (domain f)).
ir. Unfold inverse_image. ap Z_sub. 
Save.

Lemma inverse_image_inc : (a,f,x:E)
(inc x (domain f)) -> (inc (V x f) a) -> 
(inc x (inverse_image a f)). 
ir. Unfold inverse_image. ap Z_inc. am.
am. Save. 

Lemma inverse_image_pr : (a,f,x:E)(inc x (inverse_image a f))
-> (inc (V x f) a). 
ir. Unfold inverse_image in H. Ztac. 
Save. 




Definition create := [x:E;p:E -> E]
(Image.create x [y:E](pair y (p y))).


Lemma elt_rewrite : (x:E; p: E -> E; y:E)
(inc y (create x p)) -> y == (pair (pr1 y) (p (pr1 y))).
ir. Unfold create in H. Pose (Image.ex H).
nin e. xd. Assert (pr1 y) == x0.
Rewrite <- H1. ap pr1_pair. Rewrite H2. au.
Save. 

Lemma create_axioms : (p:E-> E; x:E)(axioms (create x p)).
ir. Unfold axioms; xd.
ir. ap pair_recov. Unfold create in H. 
Pose (Image.ex H). nin e. xd. 
Rewrite <- H1. ap pair_is_pair. 
ir. Unfold create in H. 
Unfold create in H0. Pose (Image.ex H).
Pose (Image.ex H0). nin e. nin e0. 
xd. Rewrite <- H5. Assert x1 == x2. 
Transitivity (pr1 x0). Rewrite <- H5. 
sy; ap pr1_pair. Rewrite H1. Rewrite <- H4. 
ap pr1_pair. Rewrite H6; am. Save. 

Lemma create_inc : (x,y:E; hyp : (inc y x);
p: E -> E; z:E) 
(pair y (p y)) == z -> (inc z (create x p)). 
ir. Unfold create. ap Image.show_inc.
Apply exists_intro with y; xd. 
Save. 

Lemma create_domain : (x:E;p:E -> E)(domain (create x p)) == x.
ir. Unfold domain. ap extensionality; Unfold sub; ir.
Pose (Image.ex H); nin e; xd. 
Unfold create in H0; Pose (Image.ex H0); nin e; xd.
Rewrite <- H1. Assert (pr1 x1) == x2. 
Rewrite <- H3; ap pr1_pair. Rewrite H4; au. 
ap Image.show_inc. Apply exists_intro with
(pair x0 (p x0)). xd. 
ap '(create_inc H); au. ap pr1_pair. Save.




Lemma create_V_apply : (x:E; p: E-> E; y,z:E)
(inc y x) -> (p y) == z -> (V y (create x p)) == z.
ir. Assert (inc (pair y (V y (create x p))) (create x p)).
ap V_inc. Apply exists_intro with (p y). 
ap '(create_inc H). tv. tv. 
Assert (axioms (create x p)). ap create_axioms. 
Unfold axioms in H2; xd. 
Assert (pair y (V y (create x p))) == (pair y z). 
ap H3. ap V_inc. Apply exists_intro with (p y). 
ap '(create_inc H). tv. tv. 
ap '(create_inc H). Rewrite H0; tv. Rewrite pr1_pair.
Rewrite pr1_pair. tv. Transitivity (pr2 (pair y z)). 
Rewrite <- H4. sy; ap pr2_pair. 
ap pr2_pair. Save. 

Lemma create_V_rewrite : (x:E; p: E -> E; y: E)
(inc y x) -> (V y (create x p)) == (p y). 
ir. ap create_V_apply; au. Save. 


Lemma create_range : (p:E-> E; x:E)(range (create x p)) ==
(Image.create x p).
ir. Unfold range. ap extensionality; Unfold sub; ir.
Pose (Image.ex H); nin e; xd. ap Image.show_inc. 
Unfold create in H0. Pose (Image.ex H0); nin e; xd.
Apply exists_intro with x2. xd.
Rewrite <- H1. Rewrite <- H3. sy; ap pr2_pair. 
Pose (Image.ex H); nin e; xd. 
ap Image.show_inc. Apply exists_intro with (pair x1 x0). 
xd. ap '(create_inc H0). Rewrite H1. tv. 
ap pr2_pair. 
Save.

Lemma create_recovers : (f:E)(axioms f) -> 
(create (domain f) [x:E](V x f)) == f.
ir. ap function_extensionality. 
ap create_axioms. am. ir. 
Unfold defined in H0. xd. Unfold defined.
xd. Rewrite create_domain in H1. am.
ir. Unfold defined in H0. xd. 
Unfold defined; xd. ap create_axioms. 
Rewrite create_domain. am. 
ir. Unfold defined in H0; xd. Rewrite
create_domain in H1. ap create_V_apply; au. 
Save. 


Lemma create_V_defined : (x:E; p: E -> E; y: E)
(defined (create x p) y) -> (V y (create x p)) == (p y). 
ir. ap create_V_apply. Unfold defined in H. 
xd. Rewrite create_domain in H0. am. 
tv. Save. 


Lemma create_extensionality : (a,b:E; f,g:E1)a==b ->
((x:E)(inc x a) -> (inc x b) -> (f x) == (g x)) -> (create a f) == (create b g).
ir.
Assert (axioms (create a f)).
ap create_axioms.

Assert (axioms (create b g)).
ap create_axioms.

ap function_extensionality; au.
Unfold defined; ir.
xd.
Rewrite -> create_domain.
Rewrite <- H.
Rewrite -> create_domain in H4.
am.

Unfold defined.
ir; xd.
Rewrite -> create_domain.
Rewrite -> create_domain in H4.
Rewrite -> H.
am.

ir.
Assert (inc x a).
Unfold defined in H3.
xd.
Rewrite -> create_domain in H4; am.

Repeat Rewrite -> create_V_rewrite.
ap H0.
am.

Rewrite <- H.
am.

Rewrite <- H.
am.

am.
Save.

Lemma create_create : (a:E; f:E1)(create a [x:E](V x (create a f))) == (create a f).
ir.
ap create_extensionality.
tv.

ir.
ap create_V_rewrite.
am.
Save.


Definition composable := [f,g:E]
(A (axioms f)
(A (axioms g)
   (sub (range g) (domain f))
)). 



Definition compose := [f,g:E]
(create (inverse_image (domain f) g) [y:E](V (V y g) f)).

Lemma compose_axioms : (f,g:E)(axioms (compose f g)).
ir. Unfold compose. 
ap create_axioms. Save. 


Lemma compose_domain : (f,g:E)
(domain (compose f g)) ==
(inverse_image (domain f) g).
ir. Unfold compose. 
Rewrite create_domain. tv. 
Save.

Lemma composable_domain : (f,g:E)(composable f g) -> 
(domain (compose f g)) == (domain g). 
ir. Unfold compose. 
Rewrite create_domain. ap extensionality. 
ap inverse_image_sub. 
Unfold sub; ir. ap inverse_image_inc. am.
Unfold composable in H. xd. 
ap H2. ap range_inc. am. 
Apply exists_intro with x. xd. Save. 



Lemma compose_ev : (x,f,g:E)(inc x (domain (compose f g))) ->
(V x (compose f g)) == (V (V x g) f).
ir. Unfold compose. 
Unfold compose in H. 
Rewrite create_domain in H. ap create_V_apply. 
am. tv. Save. 



Definition identity [x:E] := (create x [y:E]y).


Lemma identity_axioms : (x:E)(axioms (identity x)). 
ir; Unfold identity; ap create_axioms. 
Save. 


Lemma identity_domain : (x:E)(domain (identity x)) == x.
ir; Unfold identity; Rewrite create_domain; tv. 
Save. 


Lemma identity_ev : (x,a:E)(inc x a) -> (V x (identity a)) == x.
ir. Unfold identity. ap create_V_apply; au. 
Save.


End Function.

Syntactic Definition L := Function.create.




Module Transformation.


Definition covers := [a,b:E; f:E -> E](x:E)(inc x b) -> (exists 
[y:E](A (inc y a)  (f y) == x)).
Definition injects := [a:E; f:E-> E](x,y:E)(inc x a) -> (inc y a) -> 
(f x) == (f y) -> x == y.


Definition inverse := [a:E; f:E -> E;y:E](choose [x:E]
(A (inc x a)  (f x) == y)).


Definition axioms := [a,b:E; f:E -> E](x:E)(inc x a) -> (inc (f x) b).

Lemma compose_axioms : (a,b,c:E;f,g: E->E)(axioms b c f) -> (axioms a b 
g) ->
(axioms a c [x:E](f (g x))).
ir.
Unfold axioms.
ir.
Unfold axioms in H.
Unfold axioms in H0.
au.
Save.


Lemma identity_axioms : (a:E)(axioms a a [x:E]x).
ir.
Unfold axioms.
ir.
am.
Save.

Definition surjective := [a,b:E;f: E->E]
(A (axioms a b f)
   (covers a b f)
).

Lemma surjective_inverse_axioms : (a,b:E; f:E1)(surjective a b f) -> 
(axioms b a (inverse a f)).
ir.
Unfold axioms.
ir.
Unfold inverse.
Unfold surjective in H; xd.
Unfold covers in H1; xd.
Pose (H1 x H0).
Pose (choose_pr e).
xd.
Save.

Lemma surjective_inverse_right : (a,b:E; f:E1; x:E)(surjective a b f) ->
(inc x b) -> (f (inverse a f x)) == x.
ir.
Unfold inverse.
Unfold surjective in H; xd.
Unfold covers in H1; xd.
Pose (H1 x H0).
Pose (choose_pr e).
xd.
Save.


Definition injective := [a,b:E;f:E->E]
(A (axioms a b f)
   (injects a f)
).

Definition bijective := [a,b:E;f:E-> E]
(A (axioms a b f)
(A (surjective a b f)
   (injective a b f)
)).

Definition are_inverse := [a,b:E; f,g:E1]
(A (axioms a b f)
(A (axioms b a g)
(A (x:E)(inc x a) -> (g (f x)) == x
   (y:E)(inc y b) -> (f (g y)) == y
))).

Lemma bijective_inverse : (a,b:E; f:E1)(bijective a b f) ->
(are_inverse a b f (inverse a f)).
ir.
Unfold are_inverse; xd.
Unfold bijective in H; xd.

ap surjective_inverse_axioms.
Unfold bijective in H; xd.

ir.
Unfold bijective in H; xd.
Unfold injective in H2.
xd.
ap H3.
Assert (axioms b a (inverse a f)).
ap surjective_inverse_axioms; au.

Unfold axioms in H4.
ap H4.
ap H2.
am.

am.

Pose surjective_inverse_right.
Assert (inc (f x) b).
ap H2; au.

Pose (e ? ? ? ? H1 H4).
am.

ir.
Unfold bijective in H; xd.
Apply surjective_inverse_right with b.
am.

am.
Save.

Lemma inverse_bijective : (a,b:E; f,g:E1)(are_inverse a b f g) -> (bijective a b f).
ir.
Unfold bijective.
Unfold are_inverse in H.
xd.
Unfold surjective; xd.
Unfold covers.
ir.
Apply exists_intro with (g x).
xd.

Unfold injective; xd.
Unfold injects; ir.
Rewrite <- H1.
Rewrite <- H5.
Rewrite -> H1; au.

am.
Save. 


End Transformation.


Module Map.

Definition axioms := [a,b,f:E] 
(A (Function.axioms f)
(A (Function.domain f) == a
   (sub (Function.range f) b)
)).

Lemma compose_axioms : (a,b,c,f,g: E)(axioms b c f) -> (axioms a b g) -> 
(axioms a c (Function.compose f g)).
ir. Unfold axioms in H H0; xd. 
Assert (Function.composable f g). Unfold Function.composable. 
xd. Rewrite H2; am. 
Unfold axioms; xd. ap Function.compose_axioms.
Rewrite Function.composable_domain; au. 
Unfold sub; ir. 
Assert (Function.axioms (Function.compose f g)). 
ap Function.compose_axioms. Pose (Function.range_ex H7 H6). 
nin e; xd. Pose (Function.compose_ev H8). 
Rewrite H9 in e. Rewrite e. ap H4. ap Function.range_inc. 
am. Apply exists_intro with (V x0 g); xd. 
Unfold Function.composable in H5; xd. 
ap H11. ap Function.range_inc. am. 
Apply exists_intro with x0; xd. 
Assert (Function.domain (Function.compose f g)) ==
(Function.domain g). 
ap Function.composable_domain. 
Unfold Function.composable; xd. Rewrite <- H12. 
am. Save. 



Lemma identity_axioms : (a:E)(axioms a a (Function.identity a)).
ir. Unfold axioms; xd. ap Function.identity_axioms. 
ap Function.identity_domain. Unfold sub; ir. 
Assert (Function.axioms (Function.identity a)). 
ap Function.identity_axioms. Pose (Function.range_ex H0 H). 
nin e; xd. Rewrite Function.identity_domain in H1. 
Rewrite Function.identity_ev in H2. Rewrite <- H2; am. 
am. Save. 



Definition surjective := [a,b,f: E]
(A (axioms a b f)
   (Transformation.covers a b [x:E](V x f))
).

Definition injective := [a,b,f:E]
(A (axioms a b f)
   (Transformation.injects a [x:E](V x f))
).

Definition bijective := [a,b,f:E]
(A (axioms a b f)
(A (surjective a b f)
   (injective a b f)
)).


End Map.

Module Bounded.

Definition property := [p:EP; x:E](y:E)
(A (p y) -> (inc y x) (inc y x) -> (p y)). 


Definition axioms := [p:E -> Prop](exists (property p)).


Definition create := [p:E->Prop] (choose (property p)). 


Lemma criterion : (p:E -> Prop)(exists [x:E]((y:E)(p y) -> 
(inc y x))) -> (axioms p). 
ir. nin H. Unfold axioms.
EApply exists_intro with (Z x p). Unfold property.
ir; xd; ir. 
ap Z_inc. ap H; au. au. 
Apply Z_pr with x. am. Save. 



Lemma lem1 : (p:E-> Prop; y:E)(axioms p) -> 
(inc y (create p)) -> (p y).
ir. Unfold create in H0. Unfold axioms in H. 
Pose (choose_pr H). Unfold property in H0. 
Unfold property in (Type of p0). Pose (p0 y). 
xd. Save. 

Lemma lem2 : (p:E -> Prop; y:E)(axioms p) -> (p y) -> 
(inc y (create 
p)).
ir. Unfold create. Unfold axioms in H. Pose
(choose_pr H). LetTac K:= (choose (property p)). Unfold property
in (Type of p0). Pose (p0 y); xd. Save. 

Lemma inc_create : (p:E->Prop; y:E)(axioms p) -> 
(inc y (create p)) == (p y). 
ir. 
ap iff_eq; ir. ap lem1; am. 
ap lem2; am. 
Save. 

Lemma trans_criterion : (p:E->Prop; f:E1; x:E)
((y:E)(p y) -> (exists [z:E](A (inc z x) (f z)== y))) ->
(axioms p).
ir. 
ap criterion. 
sh '(Image.create x f). 
ir. ap Image.show_inc. ap H. am. 
Save. 

Lemma little_criterion : (p:E->Prop; x:E; f:x->E)
((y:E)(p y) -> (exT ? [a:x](f a) == y)) ->
(axioms p). 
ir. 
ap criterion; sh '(IM f). 
ir. ap IM_inc. ap H; am. 
Save. 


End Bounded.


Module Quotient.


Definition is_part := [a:E; r: E -> E -> Prop; y:E]
(A (sub y a)
(A (x,z:E)(inc x y) -> (r x z) -> (inc z a) -> (inc z  y)
   (x,z : E)(inc x y) -> (r z x) -> (inc z a) -> (inc z y)
)). 

Definition is_class := [a:E; r: E -> E -> Prop; y:E]
(A (is_part a r y)
(A (nonempty y) 
   (z:E)(is_part a r z) -> (nonempty (Intersection.intersection2 y z)) -> (sub y z)
)).

Lemma lem1 : (a:E; r: E -> E -> Prop)(is_part a r a).
ir.
Unfold is_part; xd.
Unfold sub; ir; au.
Save.

Definition parts_containing := [a:E; r:E -> E -> Prop; y:E]
(Z (Powerset.powerset a) [z:E](A (is_part a r z) (inc y z))). 


Definition class_of := [a:E; r: E -> E -> Prop; y:E]
(Intersection.intersection (parts_containing a r y)). 

Lemma inc_parts_containing : (a:E; r: E -> E -> Prop; y,z:E)
(inc y z) -> (is_part a r z) -> (inc z (parts_containing a r y)). 
ir. Unfold parts_containing. ap Z_inc. 
ap Powerset.powerset_inc. Unfold is_part in H0; xd. 
xd. Save. 

Lemma class_of_origin : (a:E; r: E-> E-> Prop; y:E)
(inc y a) -> (inc y (class_of a r y)). 
ir. Unfold class_of. ap intersection_inc. 
Apply nonempty_intro with a. ap inc_parts_containing. 
am. ap lem1. ir. 
Unfold parts_containing in H0. Pose (Z_pr H0). 
xd; au. Save. 


Lemma  class_of_sub : (a:E; r: E -> E -> Prop; y,z:E)
(inc y z) -> (is_part a r z) -> (sub (class_of a r y) z). 
ir. Unfold class_of. ap intersection_sub. 
ap inc_parts_containing; au. Save. 




Lemma class_of_part : (a:E; r: E -> E -> Prop; y:E)
(inc y a) -> (is_part a r (class_of a r y)).
ir.
Unfold is_part; xd; ir.
Unfold class_of.
ap Intersection.intersection_sub.
Unfold parts_containing.
ap Z_inc.
ap Powerset.powerset_inc.
Unfold sub; ir; au.

xd.
ap lem1.

Unfold class_of.
ap Intersection.intersection_inc.
Apply nonempty_intro with a.
Unfold parts_containing.
ap Z_inc.
ap Powerset.powerset_inc; Unfold sub; ir; au.

xd.
ap lem1.


ir.
Assert (is_part a r y0).
Unfold parts_containing in H3.
Pose _:=(Z_pr H3).
xd.

Unfold is_part in H4; xd.
Apply H5 with x.
Apply Intersection.intersection_forall with (parts_containing a r y).
Exact H0. am. am. am. 


Unfold class_of.
ap Intersection.intersection_inc.
Apply nonempty_intro with a.
Unfold parts_containing.
ap Z_inc.
ap Powerset.powerset_inc; Unfold sub; ir; au.

xd.
ap lem1.


ir.
Assert (is_part a r y0).
Unfold parts_containing in H3.
Pose _:=(Z_pr H3).
xd.

Unfold is_part in H4; xd.
Apply H6 with x.
Apply Intersection.intersection_forall with (parts_containing a r y).
Exact H0.
am. am. am.

Save.

Lemma class_of_class : (a:E; r: E -> E -> Prop; y:E)
(inc y a) -> (is_class a r (class_of a r y)).
ir.
Unfold is_class; xd; ir.
ap class_of_part.
am.

Apply nonempty_intro with y.
Unfold class_of.
ap Intersection.intersection_inc.
Apply nonempty_intro with a.
Unfold parts_containing; ap Z_inc; xd.
ap Powerset.powerset_inc; Unfold sub; ir; au.

ap lem1.

ir.
Unfold parts_containing in H0.
Pose _:=(Z_pr H0).
xd.

Unfold class_of.
ap Intersection.intersection_sub.
Unfold parts_containing.
ap Z_inc.
ap Powerset.powerset_inc.
Unfold is_part in H0.
xd.

xd.
nin H1.
Pose (Intersection.intersection2_first H1).
Pose (Intersection.intersection2_second H1).
ap excluded_middle; Unfold not; ir.
Pose (Z (class_of a r y) [v:E](inc v z) -> False). 
Assert (is_part a r e). Unfold is_part. 
xd. Apply sub_trans with (class_of a r y). 
Unfold e; ap Z_sub. Unfold sub; ir. 
Unfold class_of in H3. Apply Intersection.intersection_forall
with (parts_containing a r y). am. Unfold parts_containing. 
ap Z_inc. ap Powerset.powerset_inc; Unfold sub; ir;
au. xd; Try ap lem1; au. 

ir. Unfold e; Ztac. Unfold class_of. 
ap intersection_inc; ir. 
Apply nonempty_intro with a.
Unfold parts_containing; Ztac; xd.
ap Powerset.powerset_inc; Unfold sub; ir; au.

ap lem1. Unfold parts_containing in H6. 
Pose (Z_pr H6). xd. Assert (inc x (class_of a r y)). 
Assert (sub e (class_of a r y)). Unfold e; ap Z_sub. 
ap H9. am. Unfold class_of in H9. 
Assert (inc x y1). Apply intersection_forall with
(parts_containing a r y). am. Unfold 
parts_containing; ap Z_inc. ap powerset_inc. 
Unfold is_part in H7; xd; au. xd. 
Unfold is_part in H7; xd. Apply H11 with x;  
am. 
ir. Assert (inc x z). Unfold is_part in H0; xd. 
Apply H8 with z0; au. Assert (sub e a). 
Apply sub_trans with (class_of a r y). 
Unfold e; ap Z_sub. ap class_of_sub. 
am. ap lem1. ap H9; am. 
Unfold e in H3. Pose (Z_pr H3). 
ap f; am. 
ir. Unfold e; ap Z_inc. 
Assert (sub e (class_of a r y)). Unfold e; ap Z_sub. 
ap H6. Unfold e; ap Z_inc. 
Assert (is_part a r (class_of a r y)). ap class_of_part.
am. Unfold is_part in H7.
xd. Apply H9 with x. ap H6. am. 
am. am. ir. Assert (inc x z). 
Unfold is_part in H0; xd. Apply H8 with z0. 
am. am. Assert (sub e a). Apply sub_trans
with (class_of a r y). Unfold e; ap Z_sub. 
ap class_of_sub. am. ap lem1. ap H10;
am. Unfold e in H3. Pose (Z_pr H3). 
ap f; am. 
ir.
Assert (inc x z). Unfold is_part in H0; xd. 
Apply H7 with z0; au. Assert (sub e a).
Apply sub_trans
with (class_of a r y). Unfold e; ap Z_sub. 
ap class_of_sub. am. ap lem1.
ap H9; au. Unfold e in H3. Pose (Z_pr H3). 
ap f; au. Assert (sub (class_of a r y) e). 
ap class_of_sub. Unfold e; ap Z_inc. 
ap class_of_origin; au. am. am.
Assert (inc y0 e).
ap H4. am. Unfold e in H5. 
Pose (Z_pr H5). ap f; au. 
Save. 


Lemma class_rep_inc : (a:E; r: E -> E -> Prop;x:E)(is_class a r x)
-> (inc (rep x) x). 
ir. Unfold is_class in H. xd. Unfold rep. 
ap choose_pr. nin H0. 
Apply exists_intro with y; au. Save. 

Lemma class_eq_class_of : (a:E; r: E -> E -> Prop;y:E)
(is_class a r y) -> ((x:E)(inc x y) -> (class_of a r x) == y).
ir. ap extensionality. ap class_of_sub; au. 
Unfold is_class in H; xd; au. Unfold is_class in H. 
xd. ap H2. ap class_of_part. Unfold is_part in H; 
xd. Apply nonempty_intro with x. 
ap intersection2_inc; au. ap class_of_origin. 
Unfold is_part in H; xd. Save. 






Lemma intersecting_classes_eq : (a:E; r: E -> E -> Prop;
x,y:E)(is_class a r x) -> (is_class a r y) -> 
(nonempty (intersection2 x y)) -> x == y.
ir. Pose 
(class_eq_class_of H). Pose (class_eq_class_of H0). 
nin H1. Pose (intersection2_first H1). 
Pose (intersection2_second H1). 
Pose (e ? i). Pose (e0 ? i0).
Rewrite <- e1. Rewrite <- e2.
tv. Save.  


Lemma intersecting_classes_of_eq : (a:E; r: E -> E -> Prop; x,y:E)
(inc x a) -> (inc y a) ->
(nonempty (intersection2 (class_of a r x) (class_of a r y))) ->
(class_of a r x) == (class_of a r y).
ir.
Pose class_of_class.
Apply intersecting_classes_eq with a r; au.
Save.



Definition quotient := [a:E; r : E -> E -> Prop]
(Z (powerset a) [y:E](is_class a r y)).

Lemma in_quotient_is_class : (a:E; r: E -> E -> Prop; x:E)
(inc x (quotient a r)) -> (is_class a r x).
ir. Unfold quotient in  H. Pose (Z_pr H); au. 
Save. 

Lemma is_class_in_quotient : (a:E; r: E -> E -> Prop; x:E)
(is_class a r x) -> (inc x (quotient a r)).
ir. Unfold quotient; ap Z_inc. 
ap powerset_inc. Unfold is_class in H.
xd. Unfold is_part in H; xd; au. am. 
Save.


Lemma class_of_in_quotient : (a:E; r: E -> E -> Prop; x:E)
(inc x a) -> (inc (class_of a r x) (quotient a r)).
ir. Unfold quotient; ap Z_inc.
ap powerset_inc. ap class_of_sub; au. 
ap lem1. ap class_of_class; au. 
Save. 


Lemma inc_class_of : (a:E; r: E -> E -> Prop; x,y:E)
(inc x a) -> (inc y a) -> (r x y) -> (inc x (class_of a r y)).
ir.
Assert (is_part a r (class_of a r y)).
ap class_of_part.
am.

Unfold is_part in H2.
xd.
Pose _:=class_of_origin.
Apply H4 with y; au.
Save.

Lemma related_classes_eq : (a:E; r: E -> E -> Prop; x,y:E)
(inc x a) -> (inc y a) -> (r x y) -> 
(class_of a r x) == (class_of a r y).
ir.
ap intersecting_classes_of_eq; au.
Apply nonempty_intro with x.
Pose class_of_origin.
Pose inc_class_of.
ap intersection2_inc; au.
Save.


Definition class_in := [q,x:E](choose [y:E](A (inc y q) (inc x y))).



Lemma class_of_eq_class: (a:E; r: E -> E -> Prop; x:E)
(inc x a) -> (class_of a r x) == (class_in (quotient a r) x).
ir. ap class_eq_class_of. 
Assert (inc (class_in (quotient a r) x) (quotient a r)). 
Unfold class_in. 
Assert (exists [y:E](A (inc y (quotient a r)) (inc x y))). 
Apply exists_intro with (class_of a r x). 
xd. ap class_of_in_quotient; au. 
ap class_of_origin; au. 
Pose (choose_pr H0). xd. Unfold quotient in H0. 
Pose (Z_pr H0). am. 
Assert (exists [y:E](A (inc y (quotient a r)) (inc x y))).
Apply exists_intro with (class_of a r x). 
xd. ap class_of_in_quotient; au. 
ap class_of_origin; au. 
Pose (choose_pr H0). xd.  
Save.

Lemma class_of_rep : (a:E; r: E -> E -> Prop; x:E)
(inc x (quotient a r)) -> (class_of a r (rep x)) == x. 
ir. ap class_eq_class_of. ap  in_quotient_is_class;
au.
Assert (is_class a r x). ap  in_quotient_is_class;
au.
Unfold is_class in H0; xd. 
Unfold rep. nin H1. ap choose_pr. 
Apply exists_intro with y. am. 
Save. 


Definition is_eq_reln := [a:E; r:E -> E -> Prop]
(A (x:E)(inc x a) -> (r x x)
(A (x,y:E)(inc x a) -> (inc y a) -> (r x y) -> (r y x)
   (x,y,z:E)(inc x a) -> (inc y a) -> (inc z a) -> (r x y) -> (r y z) -> (r x z)
)).

Definition equivalent := [a:E; r:E -> E -> Prop; x,y:E]
(A (inc x a)
(A (inc y a)
   (class_of a r x) == (class_of a r y)
)).

Lemma equivalent_symm : (a:E; r: E -> E -> Prop; x,y:E)(equivalent a r x y) -> (equivalent a r y x).
ir.
Unfold equivalent in H.
Unfold equivalent. xd.
Save.

Lemma equivalent_refl : (a:E; r: E -> E -> Prop; x:E)(inc x a) -> (equivalent a r x x).
ir; Unfold equivalent; xd.
Save.

Lemma equivalent_trans : (a:E; r: E -> E -> Prop; x,y,z:E)(equivalent a r x y)-> (equivalent a r y z) ->
(equivalent a r x z).
Unfold equivalent; ir; xd.
Transitivity (class_of a r y); au.
Save.

Lemma equivalent_is_eq_reln : (a:E; r: E -> E -> Prop)(is_eq_reln a (equivalent a r)).
ir.
Unfold is_eq_reln; xd; ir.
ap equivalent_refl; au.
ap equivalent_symm; au.
Apply equivalent_trans with y; au.
Save.

Lemma related_equivalent : (a:E; r: E -> E -> Prop; x,y:E)(inc x a) -> (inc y a)
-> (r x y) -> (equivalent a r x y).
ir.
Unfold equivalent; xd.
ap intersecting_classes_of_eq; au.
Apply nonempty_intro with x.
ap intersection2_inc.
ap class_of_origin; au.
ap inc_class_of; au.
Save.

Lemma equivalent_related : (a:E; r:E -> E -> Prop; x,y:E)(is_eq_reln a r) ->
(equivalent a r x y) -> (r x y).
ir.
Unfold is_eq_reln in H; xd.
Pose z:=(Z a [u:E](r x u)).
Assert (inc y z).
Unfold equivalent in H0; xd.
Assert (sub (class_of a r y) z).
Rewrite <- H4.
ap class_of_sub.
Unfold z; Ztac.

Unfold is_part; xd.
Unfold z; ap Z_sub.

ir.
Unfold z; Ztac.
Apply H2 with x0.
am.

Assert (sub z a); [ Unfold z; ap Z_sub | ap H8; au ].

au.

Unfold z in H5; Ztac.

am.

ir.
Unfold z; Ztac.
Apply H2 with x0; au.
Assert (sub z a); [ Unfold z; ap Z_sub | ap H8; au ].

Unfold z in H5; Ztac.

ap H1; au.
Assert (sub z a); [ Unfold z; ap Z_sub | ap H8; au ].

ap H5.
ap class_of_origin.
am.

Unfold z in H3; Ztac.
Save.


Lemma equivalent_to_rep : (a:E; r: E -> E -> Prop; x:E)(inc x a) ->
(equivalent a r x (rep (class_of a r x))).
ir.
Unfold equivalent; xd.
Assert (sub (class_of a r x) a).
ap class_of_sub; au.
ap lem1.

ap H0.
ap nonempty_rep.
Apply nonempty_intro with x; ap class_of_origin.
am.

ap intersecting_classes_of_eq.
am.

Assert (sub (class_of a r x) a).
Pose _:=lem1; ap class_of_sub; au.

ap H0.
ap nonempty_rep.
Apply nonempty_intro with x; ap class_of_origin.
am.

Apply nonempty_intro with (rep (class_of a r x)).
ap intersection2_inc.
ap nonempty_rep.
Apply nonempty_intro with x; ap class_of_origin.
am.

ap class_of_origin.
Assert (sub (class_of a r x) a).
ap class_of_sub.
au.

ap lem1.

ap H0.
ap nonempty_rep.
Apply nonempty_intro with x.
ap class_of_origin.
am.
Save.

Lemma equivalent_universal : (a:E; r,s:E -> E -> Prop)(is_eq_reln a s) ->
((x,y:E)(inc x a) -> (inc y a) -> (r x y) -> (s x y)) -> 
((x,y:E)(equivalent a r x y) -> (s x y)).
ir.
Pose z:=(Z a [u:E](s x u)).
Assert (sub z a).
Unfold z; ap Z_sub.

Unfold sub in H2.
Unfold equivalent in H1; xd.
Assert (sub (class_of a r y) z).
Rewrite <- H4.
ap class_of_sub.
Unfold z; Ztac.
Unfold is_eq_reln in H; xd.

Unfold is_part; xd.
ir.
Unfold z; Ztac.
Unfold is_eq_reln in H; xd.
Apply H9 with x0; au.
Unfold z in H5; Ztac.

ir.
Unfold z; Ztac.
Unfold is_eq_reln in H; xd.
Apply H9 with x0; au.
Unfold z in H5; Ztac.

Assert (inc y z).
ap H5; ap class_of_origin.
au.

Unfold z in H6; Ztac.
Save.

Definition quotient_endo := [q:E; endo : E -> E; x:E](class_in q (endo (rep x))).

Definition endo_within := [a:E; endo : E -> E](x:E)(inc x a) -> (inc (endo x) a).

Definition endo_compatible := [a:E; r: E -> E -> Prop; endo: E -> E]
(x,y:E)(inc x a) -> (inc y a) -> (r x y) -> (r (endo x) (endo y)).

Definition endo_passes_to_quotient := [q:E; endo : E -> E]
(x,a:E)(inc x q) -> (inc a x) -> (class_in q (endo a)) == (quotient_endo q endo x).

Lemma endo_compatible_passes : (a:E; r: E -> E -> Prop; endo : E -> E)
(endo_within a endo) -> (endo_compatible a r endo) -> (endo_passes_to_quotient (quotient a r) endo).
ir.
Unfold endo_passes_to_quotient.
LetTac q:=(quotient a r).
ir.
Assert (is_class a r x).
ap in_quotient_is_class.
am.

Assert (class_of a r (rep x))==x.
ap class_of_rep.
am.

Assert (class_of a r a0)==x.
ap class_eq_class_of.
am.

am.

Pose z:=(Z a [u:E](class_in q (endo u))==(quotient_endo q endo x)).
Assert (sub z a). Unfold z; ap Z_sub.

Assert (sub (class_of a r (rep x)) z).
ap class_of_sub.
Unfold z; Ztac.
Unfold is_class in H3.
xd.
Unfold is_part in H3; xd.
ap H3.
ap nonempty_rep.
am.

Unfold is_part; xd.
ir.
Unfold z; Ztac.
Transitivity (class_in q (endo x0)).
Unfold q.
Assert (inc x0 a).
ap H6; au.

Rewrite <- class_of_eq_class.
Rewrite <- class_of_eq_class.
sy.
ap related_classes_eq.
ap H.
am.

ap H; am.

ap H0; au.

ap H.
au.

ap H; au.

Unfold z in H7; Ztac.

ir.
Unfold z; Ztac.
Transitivity (class_in q (endo x0)).
Assert (inc x0 a).
ap H6; au.

Unfold q.
Rewrite <- class_of_eq_class.
Rewrite <- class_of_eq_class.
ap related_classes_eq.
ap H; au.

ap H; au.

ap H0; au.

ap H; au.

ap H; au.

Unfold z in H7; Ztac.

Assert (inc a0 z).
ap H7.
Rewrite -> H4; au.

Unfold z in H8; Ztac.
Save.

Definition quotient_op := [q:E; op : E -> E -> E; x,y:E](class_in q (op (rep x) (rep y))).

Definition op_within := [a:E; op : E -> E -> E](x,y:E)(inc x a) -> (inc y a) -> (inc (op x y) a).

Definition op_left_compatible := [a:E; r: E -> E -> Prop; op : E -> E -> E]
(x,y,z: E)(inc x a) -> (inc y a) -> (inc z a)-> (r x z) -> (r (op x y) (op z y)).

Definition op_right_compatible := [a:E; r: E -> E -> Prop; op : E -> E -> E]
(x,y,z: E)(inc x a) -> (inc y a) -> (inc z a)-> (r y z) -> (r (op x y) (op x z)).

Definition op_passes_to_quotient := [q:E;op : E -> E -> E]
(x,y,a,b,c,d:E)(inc x q) -> (inc y q) -> (inc a x) -> (inc b y) ->
(class_in q (op a b)) == (quotient_op q op x y). 



Lemma op_left_very_compatible : (a:E; r: E -> E -> Prop; op : E -> E -> E)(op_within a op) ->
(op_left_compatible a r op) -> 
((x,b,c,d:E)(inc x (quotient a r)) -> (inc b x) -> (inc c x) -> (inc d a) ->
(class_in (quotient a r) (op b d)) == (class_in (quotient a r) (op c d))).
ir.
Pose f:=[u:E](op u d).
Assert (endo_within a f).
Unfold endo_within.
ir.
Unfold f.
ap H; au.

Assert (endo_compatible a r f).
Unfold endo_compatible.
ir.
Unfold f.
ap H0; au.

Pose (endo_compatible_passes H5 H6).
Unfold endo_passes_to_quotient in (Type of e).
Unfold f in (Type of e).
Transitivity (quotient_endo (quotient a r) [u:E](op u d) x).
ap e; au.

sy.
ap e; au.
Save. 

Lemma op_right_very_compatible : (a:E; r: E -> E -> Prop; op : E -> E -> E)(op_within a op) ->
(op_right_compatible a r op) -> 
((x,b,c,d:E)(inc x (quotient a r)) -> (inc b a) -> (inc c x) -> (inc d x) ->
(class_in (quotient a r) (op b c)) == (class_in (quotient a r) (op b d))).
ir.
Pose f:=[u:E](op b u).
Assert (endo_within a f).
Unfold endo_within.
ir.
Unfold f.
ap H; au.

Assert (endo_compatible a r f).
Unfold endo_compatible.
ir.
Unfold f.
ap H0; au.

Pose (endo_compatible_passes H5 H6).
Unfold endo_passes_to_quotient in (Type of e).
Unfold f in (Type of e).
Transitivity (quotient_endo (quotient a r) [u:E](op b u) x).
ap e; au.

sy.
ap e; au.
Save. 



Lemma op_compatible_passes : (a:E; r: E -> E -> Prop; op : E -> E -> E)(op_within a op) ->
(op_left_compatible a r op) -> (op_right_compatible a r op) -> (op_passes_to_quotient (quotient a r) op).
ir.
Unfold op_passes_to_quotient; ir.
Unfold quotient_op.
Assert (inc (rep x) x).
ap nonempty_rep.
Apply nonempty_intro with a0.
am.

Assert (inc (rep y) y).
ap nonempty_rep; Apply nonempty_intro with b; au.

Transitivity (class_in (quotient a r) (op a0 (rep y))).
Apply op_right_very_compatible with y; au.
Assert (inc x (powerset a)).
Unfold quotient in H2; Ztac.

Assert (sub x a).
ap powerset_sub.
am.

ap H9.
am.

Apply op_left_very_compatible with x; au.
Assert (sub y a).
ap powerset_sub.
Unfold quotient in H3; Ztac.

ap H8; au.
Save.

End Quotient.


Module Cartesian.

Definition in_record := [a:E; f:E1; x:E]
(A (is_pair x)
(A (inc (pr1 x) a)
   (inc (pr2 x) (f (pr1 x)))
)).

Record recordRec [a:E; f:E1]:E := {
first : a;
second : (f (R first))
}.

Definition recordMap := [a:E; f:E1; i:(recordRec a f)](pair (R (first i)) (R (second i))).

Lemma in_record_ex : (a:E; f:E1; x:E)(in_record a f x) -> (exT ? [i:(recordRec a f)](recordMap i) == x).
ir.
Unfold in_record in H; xd.
Pose u:=(B H0).
Assert (R u)==(pr1 x).
Unfold u.
ap B_eq.

Assert (inc (pr2 x) (f (R u))).
Rewrite -> H2; am.

Pose v:=(B H3).
Pose (!Build_recordRec a f u v).
Apply exT_intro with r.
Transitivity (pair (R u) (R v)).
tv.

Assert (R v)==(pr2 x).
Unfold v.
ap B_eq.

Rewrite -> H4.
Assert (R u)==(pr1 x); au.
Rewrite -> H5.
ap pair_recov.
am.
Save.

Lemma in_record_bounded : (a:E; f:E1)(Bounded.axioms (in_record a f)).
ir.
ap Bounded.criterion.
Apply exists_intro with (IM (!recordMap a f)).
ir.
ap IM_inc.
ap in_record_ex.
am.
Save.

Definition record := [a:E; f: E1](Bounded.create (in_record a f)).

Lemma record_in : (a:E; f:E1; x:E)(inc x (record a f)) -> (in_record a f x).
ir.
Unfold record in H.
Pose (in_record_bounded a f).
Pose (Bounded.lem1 a0 H).
am.
Save.

Lemma record_pr : (a:E; f:E1; x:E)(inc x (record a f)) -> 
(A (is_pair x)
(A (inc (pr1 x) a)
   (inc (pr2 x) (f (pr1 x)))
)).
ir. Pose (record_in H). am.
Save.

Lemma record_inc : (a:E; f:E1; x:E)(in_record a f x) -> (inc x (record a f)).
ir.
Unfold record.
ap Bounded.lem2.
ap in_record_bounded.
am.
Save.

Lemma record_pair_pr : (a:E; f: E1; x,y:E)(inc (pair x y) (record a f)) -> (A (inc x a) (inc y (f x))).
ir.
xd.
Pose (record_in H).
Unfold in_record in (Type of i); xd.
Rewrite -> pr1_pair in H1.
am.

Pose (record_in H).
Unfold in_record in (Type of i); xd.
Rewrite -> pr1_pair in H2.
Rewrite -> pr2_pair in H2.
am.
Save.

Lemma record_pair_inc : (a:E; f:E1; x,y:E)(inc x a) -> (inc y (f x)) -> (inc (pair x y) (record a f)).
ir.
ap record_inc.
Unfold in_record; xd.
ap pair_is_pair.
Rewrite -> pr1_pair; am.
Rewrite -> pr2_pair; Rewrite -> pr1_pair; am.
Save.

Definition product := [a,b:E](record a [x:E]b).

Lemma product_pr : (a,b,u:E)(inc u (product a b)) ->
(A (is_pair u)
(A (inc (pr1 u) a)
   (inc (pr2 u) b)
)).
ir. Unfold product in H. Pose (record_pr H). xd.
Save.

Lemma product_inc : (a,b,u:E)(is_pair u) -> (inc (pr1 u) a) -> (inc (pr2 u) b) -> (inc u (product a b)).
ir. Unfold product. ap record_inc. Unfold in_record; xd.
Save.

Lemma product_pair_pr : (a,b,x,y:E)(inc (pair x y) (product a b)) -> (A (inc x a) (inc y b)).
ir. Unfold product in H. Pose (record_pair_pr H). am.
Save.

Lemma product_pair_inc : (a,b,x,y:E)(inc x a) -> (inc y b) -> (inc (pair x y) (product a b)).
ir. Unfold product. ap record_pair_inc; au.
Save.


End Cartesian.

Export Cartesian.

Module Function_Set.

Definition in_function_set := [a:E; f:E1; u:E]
(A (Function.axioms u)
(A (Function.domain u) == a
   (y:E)(inc y a) -> (inc (V y u) (f y))
)).

Lemma in_fs_sub_record : (a:E; f:E1; u:E)(in_function_set a f u) -> (sub u (record a f)).
ir.
Unfold in_function_set in H; xd.
Unfold sub; ir.
Pose (Function.pr2_V H H2).
Assert (Function.axioms u).
am.

Unfold Function.axioms in H3; xd.
Pose (H3 ? H2).
Rewrite <- e0.
ap record_pair_inc.
Rewrite <- H0.
ap Function.lem2; au.

Rewrite -> e.
ap H1.
Rewrite <- H0.
ap Function.lem2; au.
Save.

Lemma in_fs_eq_L : (a:E; f:E1; u:E)(in_function_set a f u) -> u == (L a [y:E](V y u)).
ir.
Unfold in_function_set in H; xd.
Rewrite <- H0.
sy.
ap Function.create_recovers.
am.
Save.

Lemma in_fs_for_L : (a:E; f,v:E1)((y:E)(inc y a) -> (inc (v y) (f y))) -> (in_function_set a f (L a v)).
ir.
Unfold in_function_set; xd.
ap Function.create_axioms.

ap Function.create_domain.

ir.
Rewrite -> Function.create_V_rewrite.
ap H; au.

am.
Save.

Lemma in_fs_bounded : (a:E; f:E1)(Bounded.axioms (in_function_set a f)).
ir.
ap Bounded.criterion.
Apply exists_intro with (powerset (record a f)).
ir.
ap powerset_inc.
ap in_fs_sub_record; au.
Save.

Definition function_set := [a:E; f:E1](Bounded.create (in_function_set a f)).

Lemma function_set_iff : (a:E; f:E1; u:E)(inc u (function_set a f)) <-> (in_function_set a f u).
ir.
Unfold iff; xd; ir.
Unfold function_set in H.
ap Bounded.lem1.
ap in_fs_bounded.

am.

Unfold function_set.
ap Bounded.lem2.
ap in_fs_bounded.

am.
Save.

Lemma function_set_sub_powerset_record : (a:E; f:E1)(sub (function_set a f) (powerset (record a f))).
ir.
Unfold sub; ir.
Pose (function_set_iff a f x).
Unfold iff in (Type of i); xd.
Pose (H0 H).
ap powerset_inc.
ap in_fs_sub_record; au.
Save.

Lemma function_set_pr : (a:E; f:E1; u:E)(inc u (function_set a f)) -> 
(A (in_function_set a f u)
(A (Function.axioms u)
(A (Function.domain u) == a
   (y:E)(inc y a) -> (inc (V y u) (f y))
))).
ir.
Assert (in_function_set a f u).
Pose (function_set_iff a f u).
Unfold iff in (Type of i); xd.

Unfold in_function_set in H0; xd.
Unfold in_function_set; xd.
Save.

Lemma function_set_inc : (a:E; f:E1; u:E)(Function.axioms u) -> (Function.domain u) == a ->
((y:E)(inc y a) -> (inc (V y u) (f y))) -> (inc u (function_set a f)).
ir.
Pose (function_set_iff a f u).
Unfold iff in (Type of i); xd.
ap H3.
Unfold in_function_set; xd.
Save.


Lemma in_function_set_inc : (a:E; f:E1; u:E)(in_function_set a f u) ->(inc u (function_set a f)).
ir.
Pose (function_set_iff a f u).
Unfold iff in (Type of i); xd.
Save.


End Function_Set.