DEFINITION leq_ahead_false_1()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(leq g (AHead a1 a2) a1)→∀P:Prop.P
BODY =
Show proof