DEFINITION sym_not_eq()
TYPE =
       ∀A:Set.∀x:A.∀y:A.(not (eq A x y))→(not (eq A y x))
BODY =
        assume A: Set
        assume x: A
        assume y: A
        suppose h1: not (eq A x y)
          we must prove not (eq A y x)
          or equivalently (eq A y x)→False
          suppose h2: eq A y x
             we proceed by induction on h2 to prove eq A x y
                case refl_equal : ⇒
                   the thesis becomes eq A y y
                      by (refl_equal . .)
eq A y y
             we proved eq A x y
             by (h1 previous)
             we proved False
          we proved (eq A y x)→False
          that is equivalent to not (eq A y x)
       we proved ∀A:Set.∀x:A.∀y:A.(not (eq A x y))→(not (eq A y x))