(asucc g a3) (asucc g a4))).(\lambda (a5: A).(\lambda (a6: A).(\lambda (_:
(leq g a5 a6)).(\lambda (H3: (leq g (asucc g a5) (asucc g a6))).(leq_head g
a3 a4 H0 (asucc g a5) (asucc g a6) H3))))))))) a1 a2 H)))).
(asucc g a3) (asucc g a4))).(\lambda (a5: A).(\lambda (a6: A).(\lambda (_:
(leq g a5 a6)).(\lambda (H3: (leq g (asucc g a5) (asucc g a6))).(leq_head g
a3 a4 H0 (asucc g a5) (asucc g a6) H3))))))))) a1 a2 H)))).