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 =
Show proof