-x3))) (sym_eq C (CHead x0 k x3) (CHead x4 k x3) (sym_eq C (CHead x4 k x3)
-(CHead x0 k x3) (sym_eq C (CHead x0 k x3) (CHead x4 k x3) (f_equal3 C K T C
-CHead x0 x4 k k x3 x3 (H x0 (r k n) h H5 x4 H8) (refl_equal K k) (refl_equal
-T x3))))) x5 (lift_inj x5 x3 h (r k n) H11))))) x1 H6)) x2 H3))))))
-(drop_gen_skip_l c0 x1 t h n k H1))))))) (drop_gen_skip_l c0 x2 t h n k
-H2)))))))) d))))))) c).
+x3))) (f_equal3 C K T C CHead x4 x0 k k x3 x3 (sym_eq C x0 x4 (H x0 (r k n) h
+H5 x4 H8)) (refl_equal K k) (refl_equal T x3)) x5 (lift_inj x5 x3 h (r k n)
+H11))))) x1 H6)) x2 H3)))))) (drop_gen_skip_l c0 x1 t h n k H1)))))))
+(drop_gen_skip_l c0 x2 t h n k H2)))))))) d))))))) c).