DEFINITION leq_gen_head1()
TYPE =
       ∀g:G
         .∀a1:A
           .∀a2:A
             .∀a:A
               .leq g (AHead a1 a2) a
                 →ex3_2 A A λa3:A.λ:A.leq g a1 a3 λ:A.λa4:A.leq g a2 a4 λa3:A.λa4:A.eq A a (AHead a3 a4)
BODY =
Show proof