DEFINITION lift_d()
TYPE =
       ∀t:T
         .∀h:nat
           .∀k:nat
             .∀d:nat
               .∀e:nat
                 .le e d
                   →eq T (lift h (plus k d) (lift k e t)) (lift k e (lift h d t))
BODY =
Show proof