\forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d:
nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e
(lift h d t)) (lift (plus k h) d t))))))))
\forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d:
nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e
(lift h d t)) (lift (plus k h) d t))))))))