DEFINITION lift_tlt_dx()
TYPE =
       ∀k:K.∀u:T.∀t:T.∀h:nat.∀d:nat.(tlt t (THead k u (lift h d t)))
BODY =
Show proof