DEFINITION leq_asucc()
TYPE =
∀
g:
G
.
∀
a:
A
.(
ex
A
λ
a0:
A
.
leq
g a (
asucc
g a0))
BODY =
Show proof