helm/matita/tests/simpl.ma

   1 set "baseuri" "cic:/matita/tests/simpl/".
   2
   3 alias id "not" = "cic:/Coq/Init/Logic/not.con".
   4 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
   5 theorem a :
   6  \forall A:Set.
   7  \forall x,y : A.
   8  not (x = y) \to not(y = x).
   9 intros.
  10 simplify.
  11 intro. apply H.
  12 symmetry.
  13 exact H1.
  14 qed.