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