DEFINITION leq_eq()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(eq A a1 a2)→(leq g a1 a2)
BODY =
        assume g: G
        assume a1: A
        assume a2: A
        suppose H: eq A a1 a2
          we proceed by induction on H to prove leq g a1 a2
             case refl_equal : ⇒
                the thesis becomes leq g a1 a1
                   by (leq_refl . .)
leq g a1 a1
          we proved leq g a1 a2
       we proved ∀g:G.∀a1:A.∀a2:A.(eq A a1 a2)→(leq g a1 a2)