(lift (S O) (s k d) x0)) t2)) (refl_equal T (THead k (lift (S O) d x) (lift
(S O) (s k d) x0))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O)
d)))) t0 H3) t1 H6))) H5)) H4))))) H2)) H1))))))))) t).
(lift (S O) (s k d) x0)) t2)) (refl_equal T (THead k (lift (S O) d x) (lift
(S O) (s k d) x0))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O)
d)))) t0 H3) t1 H6))) H5)) H4))))) H2)) H1))))))))) t).