DEFINITION subst_subst0()
TYPE =
       ∀v:T.∀t1:T.∀t2:T.∀d:nat.(subst0 d v t1 t2)→(eq T (subst d v t1) (subst d v t2))
BODY =
Show proof