DEFINITION lift_weight()
TYPE =
       ∀t:T.∀h:nat.∀d:nat.(eq nat (weight (lift h d t)) (weight t))
BODY =
Show proof