DEFINITION subst_lift_SO()
TYPE =
       ∀v:T.∀t:T.∀d:nat.(eq T (subst d v (lift (S O) d t)) t)
BODY =
Show proof