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