DEFINITION lift_inj()
TYPE =
       ∀x:T.∀t:T.∀h:nat.∀d:nat.(eq T (lift h d x) (lift h d t))→(eq T x t)
BODY =
Show proof