-a0))).(leq_ahead_false g a a0 H13 P))) a6 (sym_eq A a6 (asucc g a0) H12))) a4
-(sym_eq A a4 a H11))) H10))) a5 (sym_eq A a5 a2 H8))) a3 (sym_eq A a3 (AHead
-a a0) H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (AHead (AHead a a0) a2))
-(refl_equal A (AHead a (asucc g a0)))))))))))) a1)).
+a0))).(leq_ahead_false_1 g a a0 H13 P))) a6 (sym_eq A a6 (asucc g a0) H12)))
+a4 (sym_eq A a4 a H11))) H10))) a5 (sym_eq A a5 a2 H8))) a3 (sym_eq A a3
+(AHead a a0) H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (AHead (AHead a
+a0) a2)) (refl_equal A (AHead a (asucc g a0)))))))))))) a1)).