-(lt_le_S (s k i0) (s k d) (s_lt k i0 d H4)) h) (minus d (S i0)) (minus_s_s k
-d (S i0)))) (lift h d (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d
-(THead k u1 t0)) (lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
+(s_lt k i0 d H4) h) (minus d (S i0)) (minus_s_s k d (S i0)))) (lift h d
+(THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead k u1 t0))
+(lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).