( True : Prop ) 

( True_intro : ?? True ) 

---

( False : Prop ) 

( False_elim : False -> ( { A : Prop } A ) ) 

---

( Implies : Prop -> Prop -> Prop ) 

( Implies_intro : { A,B : Prop } (A -> B) -> (Implies A B) )

( Implies_elim : { A,B : Prop } (Implies A B) -> A -> B )

***( Implies_eq : {A,B : Prop}{F : A -> B}{M : A}
  (EQ (Implies_elim A B (Implies_intro A B F) M) (F M)) )

---

( And : Prop -> Prop -> Prop ) 

( And_intro : ?? { A,B : Prop } A -> B -> (And A B) ) 

( And_elim_l : {A,B : Prop} (And A B) -> A ) 
( And_elim_r : {A,B : Prop} (And A B) -> B ) 

***( And_eq_l : {A,B : Prop} {a : A}{b : B}
   (EQ (And_elim_l A B (And_intro A B a b)) a) )
***( And_eq_r : {A,B : Prop} {a : A}{b : B}
   (EQ (And_elim_r A B (And_intro A B a b)) b) )

( And_elim : {A,B,C : Prop} (And A B) -> (A -> B -> C) -> C )

***( And_eq : {A,B,C : Prop}{a : A}{b : B}{F : A -> B -> C}
  (EQ (And_elim A B C (And_intro A B a b) F) (F a b)) )

---

( Or : Prop -> Prop -> Prop ) 

( Or_intro_l : ?? { A,B : Prop } A -> (Or A B) ) 
( Or_intro_r : ?? { A,B : Prop } B -> (Or A B) )

( Or_elim : { A,B,C : Prop } (Or A B) -> (A -> C) -> (B -> C) -> C ) 

***( Or_eq_l : {A,B,C : Prop}{a : A}{F : A -> C}{G : B -> C}
  (EQ (Or_elim A B C (Or_intro_l A B a) F G) (F a)) )

***( Or_eq_r : {A,B,C : Prop}{b : B}{F : A -> C}{G : B -> C}
  (EQ (Or_elim A B C (Or_intro_r A B b) F G) (G b)) )

---

( Iff : Prop -> Prop -> Prop ) 

( Iff_intro : {A,B : Prop} (A -> B) -> (B -> A) -> (Iff A B) )

( Iff_elim_lr : {A,B : Prop} (Iff A B) -> (A -> B) )
( Iff_elim_rl : {A,B : Prop} (Iff A B) -> (B -> A) )

***( Iff_eq_lr : {A,B : Prop}{F : A -> B}{G : B -> A}
    (EQ (Iff_elim_lr A B (Iff_intro A B F G)) F) )

***( Iff_eq_rl : {A,B : Prop}{F : A -> B}{G : B -> A}
    (EQ (Iff_elim_rl A B (Iff_intro A B F G)) G) )

---

( Not : Prop -> Prop ) 

( Not_intro : {A : Prop}(A -> False) -> (Not A) )

( Not_elim : {A : Prop}(Not A) -> A -> False )

***( Not_eq : {A : Prop}{F : A -> False}
  (EQ (Not_elim A (Not_intro A F)) F) )

---

( All : {U | UNIV}{T : U} (T -> Prop) -> Prop ) 

( All_intro : {U | UNIV}{T : U}{P : (T -> Prop)}({x : T} (P x)) -> (All ? P) )

( All_elim : {U | UNIV}{T : U}{P : (T -> Prop)} (All ? P) -> {x : T} (P x) ) 

***( All_eq : {U : UNIV}{T : U}{P : (T -> Prop)}{F : {x : T}(P x)}{M : T}
  (EQ (All_elim P (All_intro P F) M) (F M)) )

---

( Ex : {U | UNIV}{T : U} (T -> Prop) -> Prop )  

( Ex_intro : {U | UNIV}{T : U}{x : T}{P : (T -> Prop)} (P x) -> (Ex ? P) ) 

( Ex_elim : {U | UNIV}{T : U}{P : (T -> Prop)} (Ex ? P) -> {A : Prop} ( {x : T} (P x) -> A ) -> A ) 

***( Ex_eq : {U : UNIV}{T : U}{P : (T -> Prop)}{M : T}{p : (P M)}{A : Prop}{F : {x : T} (P x) -> A}
  (EQ (Ex_elim P (Ex_intro M P p) A F) (F M p)) )

---

( And3 : Prop -> Prop -> Prop -> Prop ) 

---

( Or3 : Prop -> Prop -> Prop -> Prop ) 

---

( EM : {P : Prop} (Or P (Not P)) )

( done )