DEFINITION sym_eq()
TYPE =
       ∀A:Set.∀x:A.∀y:A.(eq A x y)→(eq A y x)
BODY =
Show proof