DEFINITION trans_eq()
TYPE =
       ∀A:Set.∀x:A.∀y:A.∀z:A.(eq A x y)→(eq A y z)→(eq A x z)
BODY =
        assume A: Set
        assume x: A
        assume y: A
        assume z: A
        suppose H: eq A x y
        suppose H0: eq A y z
          we proceed by induction on H0 to prove eq A x z
             case refl_equal : ⇒
                the thesis becomes the hypothesis H
          we proved eq A x z
       we proved ∀A:Set.∀x:A.∀y:A.∀z:A.(eq A x y)→(eq A y z)→(eq A x z)