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