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