DEFINITION subst1_trans()
TYPE =
       ∀t2:T.∀t1:T.∀v:T.∀i:nat.(subst1 i v t1 t2)→∀t3:T.(subst1 i v t2 t3)→(subst1 i v t1 t3)
BODY =
        assume t2: T
        assume t1: T
        assume v: T
        assume i: nat
        suppose H: subst1 i v t1 t2
          we proceed by induction on H to prove ∀t3:T.(subst1 i v t2 t3)→(subst1 i v t1 t3)
             case subst1_refl : ⇒
                the thesis becomes ∀t3:T.(subst1 i v t1 t3)→(subst1 i v t1 t3)
                    assume t3: T
                    suppose H0: subst1 i v t1 t3
                      consider H0
∀t3:T.(subst1 i v t1 t3)→(subst1 i v t1 t3)
             case subst1_single : t3:T H0:subst0 i v t1 t3 ⇒
                the thesis becomes ∀t4:T.∀H1:(subst1 i v t3 t4).(subst1 i v t1 t4)
                    assume t4: T
                    suppose H1: subst1 i v t3 t4
                      we proceed by induction on H1 to prove subst1 i v t1 t4
                         case subst1_refl : ⇒
                            the thesis becomes subst1 i v t1 t3
                               by (subst1_single . . . . H0)
subst1 i v t1 t3
                         case subst1_single : t0:T H2:subst0 i v t3 t0 ⇒
                            the thesis becomes subst1 i v t1 t0
                               by (subst0_trans . . . . H0 . H2)
                               we proved subst0 i v t1 t0
                               by (subst1_single . . . . previous)
subst1 i v t1 t0
                      we proved subst1 i v t1 t4
∀t4:T.∀H1:(subst1 i v t3 t4).(subst1 i v t1 t4)
          we proved ∀t3:T.(subst1 i v t2 t3)→(subst1 i v t1 t3)
       we proved ∀t2:T.∀t1:T.∀v:T.∀i:nat.(subst1 i v t1 t2)→∀t3:T.(subst1 i v t2 t3)→(subst1 i v t1 t3)