+set "baseuri" "cic:/matita/tests/simpl/".
+
alias id "not" = "cic:/Coq/Init/Logic/not.con".
alias symbol "eq" (instance 0) = "leibnitz's equality".
theorem a :
\forall A:Set.
\forall x,y : A.
not (x = y) \to not(y = x).
-intro.
+intros.
simplify.
+intro. apply H.
+symmetry.
+exact H1.
+qed.