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