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