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