DEFINITION subst1_subst1_back()
TYPE =
       ∀t1:T
         .∀t2:T
           .∀u2:T
             .∀j:nat
               .subst1 j u2 t1 t2
                 →∀u1:T.∀u:T.∀i:nat.(subst1 i u u2 u1)→(ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t2 t)
BODY =
        assume t1: T
        assume t2: T
        assume u2: T
        assume j: nat
        suppose H: subst1 j u2 t1 t2
          we proceed by induction on H to prove ∀u1:T.∀u:T.∀i:nat.(subst1 i u u2 u1)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t2 t0)
             case subst1_refl : ⇒
                the thesis becomes ∀u1:T.∀u:T.∀i:nat.(subst1 i u u2 u1)→(ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t1 t)
                    assume u1: T
                    assume u: T
                    assume i: nat
                    suppose : subst1 i u u2 u1
                      (h1) 
                         by (subst1_refl . . .)
subst1 j u1 t1 t1
                      end of h1
                      (h2) 
                         by (subst1_refl . . .)
subst1 (S (plus i j)) u t1 t1
                      end of h2
                      by (ex_intro2 . . . . h1 h2)
                      we proved ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t1 t
∀u1:T.∀u:T.∀i:nat.(subst1 i u u2 u1)→(ex2 T λt:T.subst1 j u1 t1 t λt:T.subst1 (S (plus i j)) u t1 t)
             case subst1_single : t3:T H0:subst0 j u2 t1 t3 ⇒
                the thesis becomes ∀u1:T.∀u:T.∀i:nat.∀H1:(subst1 i u u2 u1).(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t3 t0)
                    assume u1: T
                    assume u: T
                    assume i: nat
                    suppose H1: subst1 i u u2 u1
                      we proceed by induction on H1 to prove ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t3 t0
                         case subst1_refl : ⇒
                            the thesis becomes ex2 T λt:T.subst1 j u2 t1 t λt:T.subst1 (S (plus i j)) u t3 t
                               (h1) 
                                  by (subst1_single . . . . H0)
subst1 j u2 t1 t3
                               end of h1
                               (h2) 
                                  by (subst1_refl . . .)
subst1 (S (plus i j)) u t3 t3
                               end of h2
                               by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 j u2 t1 t λt:T.subst1 (S (plus i j)) u t3 t
                         case subst1_single : t0:T H2:subst0 i u u2 t0 ⇒
                            the thesis becomes ex2 T λt:T.subst1 j t0 t1 t λt:T.subst1 (S (plus i j)) u t3 t
                               by (subst0_subst0_back . . . . H0 . . . H2)
                               we proved ex2 T λt:T.subst0 j t0 t1 t λt:T.subst0 (S (plus i j)) u t3 t
                               we proceed by induction on the previous result to prove ex2 T λt:T.subst1 j t0 t1 t λt:T.subst1 (S (plus i j)) u t3 t
                                  case ex_intro2 : x:T H3:subst0 j t0 t1 x H4:subst0 (S (plus i j)) u t3 x ⇒
                                     the thesis becomes ex2 T λt:T.subst1 j t0 t1 t λt:T.subst1 (S (plus i j)) u t3 t
                                        (h1) 
                                           by (subst1_single . . . . H3)
subst1 j t0 t1 x
                                        end of h1
                                        (h2) 
                                           by (subst1_single . . . . H4)
subst1 (S (plus i j)) u t3 x
                                        end of h2
                                        by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.subst1 j t0 t1 t λt:T.subst1 (S (plus i j)) u t3 t
ex2 T λt:T.subst1 j t0 t1 t λt:T.subst1 (S (plus i j)) u t3 t
                      we proved ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t3 t0
∀u1:T.∀u:T.∀i:nat.∀H1:(subst1 i u u2 u1).(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t3 t0)
          we proved ∀u1:T.∀u:T.∀i:nat.(subst1 i u u2 u1)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t2 t0)
       we proved 
          ∀t1:T
            .∀t2:T
              .∀u2:T
                .∀j:nat
                  .(subst1 j u2 t1 t2)→∀u1:T.∀u:T.∀i:nat.(subst1 i u u2 u1)→(ex2 T λt0:T.subst1 j u1 t1 t0 λt0:T.subst1 (S (plus i j)) u t2 t0)