DEFINITION subst1_ex()
TYPE =
       ∀u:T.∀t1:T.∀d:nat.(ex T λt2:T.subst1 d u t1 (lift (S O) d t2))
BODY =
Show proof