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