DEFINITION leq_refl()
TYPE =
∀
g:
G
.
∀
a:
A
.(
leq
g a a)
BODY =
Show proof