DEFINITION subst1_confluence_eq()
TYPE =
       ∀t0:T.∀t1:T.∀u:T.∀i:nat.(subst1 i u t0 t1)→∀t2:T.(subst1 i u t0 t2)→(ex2 T λt:T.subst1 i u t1 t λt:T.subst1 i u t2 t)
BODY =
        assume t0: T
        assume t1: T
        assume u: T
        assume i: nat
        suppose H: subst1 i u t0 t1
          we proceed by induction on H to prove ∀t2:T.(subst1 i u t0 t2)→(ex2 T λt3:T.subst1 i u t1 t3 λt3:T.subst1 i u t2 t3)
             case subst1_refl : ⇒
                the thesis becomes ∀t2:T.(subst1 i u t0 t2)→(ex2 T λt:T.subst1 i u t0 t λt:T.subst1 i u t2 t)
                    assume t2: T
                    suppose H0: subst1 i u t0 t2
                      by (subst1_refl . . .)
                      we proved subst1 i u t2 t2
                      by (ex_intro2 . . . . H0 previous)
                      we proved ex2 T λt:T.subst1 i u t0 t λt:T.subst1 i u t2 t
∀t2:T.(subst1 i u t0 t2)→(ex2 T λt:T.subst1 i u t0 t λt:T.subst1 i u t2 t)
             case subst1_single : t2:T H0:subst0 i u t0 t2 ⇒
                the thesis becomes ∀t3:T.∀H1:(subst1 i u t0 t3).(ex2 T λt4:T.subst1 i u t2 t4 λt4:T.subst1 i u t3 t4)
                    assume t3: T
                    suppose H1: subst1 i u t0 t3
                      we proceed by induction on H1 to prove ex2 T λt4:T.subst1 i u t2 t4 λt4:T.subst1 i u t3 t4
                         case subst1_refl : ⇒
                            the thesis becomes ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t0 t
                               (h1) 
                                  by (subst1_refl . . .)
subst1 i u t2 t2
                               end of h1
                               (h2) 
                                  by (subst1_single . . . . H0)
subst1 i u t0 t2
                               end of h2
                               by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t0 t
                         case subst1_single : t4:T H2:subst0 i u t0 t4 ⇒
                            the thesis becomes ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                               by (subst0_confluence_eq . . . . H2 . H0)
                               we proved or4 (eq T t4 t2) (ex2 T λt:T.subst0 i u t4 t λt:T.subst0 i u t2 t) (subst0 i u t4 t2) (subst0 i u t2 t4)
                               we proceed by induction on the previous result to prove ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                                  case or4_intro0 : H3:eq T t4 t2 ⇒
                                     the thesis becomes ex2 T λt5:T.subst1 i u t2 t5 λt5:T.subst1 i u t4 t5
                                        (h1) 
                                           by (subst1_refl . . .)
subst1 i u t2 t2
                                        end of h1
                                        (h2) 
                                           by (subst1_refl . . .)
subst1 i u t2 t2
                                        end of h2
                                        by (ex_intro2 . . . . h1 h2)
                                        we proved ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t2 t
                                        by (eq_ind_r . . . previous . H3)
ex2 T λt5:T.subst1 i u t2 t5 λt5:T.subst1 i u t4 t5
                                  case or4_intro1 : H3:ex2 T λt:T.subst0 i u t4 t λt:T.subst0 i u t2 t ⇒
                                     the thesis becomes ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                                        we proceed by induction on H3 to prove ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                                           case ex_intro2 : x:T H4:subst0 i u t4 x H5:subst0 i u t2 x ⇒
                                              the thesis becomes ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                                                 (h1) 
                                                    by (subst1_single . . . . H5)
subst1 i u t2 x
                                                 end of h1
                                                 (h2) 
                                                    by (subst1_single . . . . H4)
subst1 i u t4 x
                                                 end of h2
                                                 by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                                  case or4_intro2 : H3:subst0 i u t4 t2 ⇒
                                     the thesis becomes ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                                        (h1) 
                                           by (subst1_refl . . .)
subst1 i u t2 t2
                                        end of h1
                                        (h2) 
                                           by (subst1_single . . . . H3)
subst1 i u t4 t2
                                        end of h2
                                        by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                                  case or4_intro3 : H3:subst0 i u t2 t4 ⇒
                                     the thesis becomes ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                                        (h1) 
                                           by (subst1_single . . . . H3)
subst1 i u t2 t4
                                        end of h1
                                        (h2) 
                                           by (subst1_refl . . .)
subst1 i u t4 t4
                                        end of h2
                                        by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
ex2 T λt:T.subst1 i u t2 t λt:T.subst1 i u t4 t
                      we proved ex2 T λt4:T.subst1 i u t2 t4 λt4:T.subst1 i u t3 t4
∀t3:T.∀H1:(subst1 i u t0 t3).(ex2 T λt4:T.subst1 i u t2 t4 λt4:T.subst1 i u t3 t4)
          we proved ∀t2:T.(subst1 i u t0 t2)→(ex2 T λt3:T.subst1 i u t1 t3 λt3:T.subst1 i u t2 t3)
       we proved ∀t0:T.∀t1:T.∀u:T.∀i:nat.(subst1 i u t0 t1)→∀t2:T.(subst1 i u t0 t2)→(ex2 T λt3:T.subst1 i u t1 t3 λt3:T.subst1 i u t2 t3)