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 =
Show proof