(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)))).
(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)))).