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).
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).