DEFINITION asucc_inj()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(leq g (asucc g a1) (asucc g a2))→(leq g a1 a2)
BODY =
Show proof