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