(a7: A).(leq g a2 a7))) (\lambda (a6: A).(\lambda (a7: A).(eq A (AHead a3 a5)
(AHead a6 a7)))) a3 a5 H12 H10 (refl_equal A (AHead a3 a5)))))))))
H6))))))))))) y a H0))) H))))).
(a7: A).(leq g a2 a7))) (\lambda (a6: A).(\lambda (a7: A).(eq A (AHead a3 a5)
(AHead a6 a7)))) a3 a5 H12 H10 (refl_equal A (AHead a3 a5)))))))))
H6))))))))))) y a H0))) H))))).