fix

[helm.git] / helm / matita / tests / simpl.ma

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