added simpl test script

diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
new file mode 100644 (file)
index 0000000..887566f
--- /dev/null
+++ b/helm/matita/tests/simpl.ma
@@ -0,0 +1,8 @@
+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 in hyp not(x=y).