(S O) O (lift h d (lift1 p t)))) (lift h (plus (S O) d) (lift (S O) O (lift1
p t))) (lift_d (lift1 p t) h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S
d))) (lift1 (Ss p) (lift (S O) O t)) (H t))))))) hds).
(S O) O (lift h d (lift1 p t)))) (lift h (plus (S O) d) (lift (S O) O (lift1
p t))) (lift_d (lift1 p t) h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S
d))) (lift1 (Ss p) (lift (S O) O t)) (H t))))))) hds).