\forall (g: G).(\forall (a1: A).(\forall (a2: A).((eq A a1 a2) \to (leq g a1
a2))))
\def
\lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (H: (eq A a1
a2)).(eq_ind A a1 (\lambda (a: A).(leq g a1 a)) (leq_refl g a1) a2 H)))).
\forall (g: G).(\forall (a1: A).(\forall (a2: A).((eq A a1 a2) \to (leq g a1
a2))))
\def
\lambda (g: G).(\lambda (a1: A).(\lambda (a2: A).(\lambda (H: (eq A a1
a2)).(eq_ind A a1 (\lambda (a: A).(leq g a1 a)) (leq_refl g a1) a2 H)))).