From 03b76418d261acfb3b33d64283ea0269ba596859 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 24 May 2005 13:34:02 +0000
Subject: [PATCH] added simpl test script

---
 helm/matita/tests/simpl.ma | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 helm/matita/tests/simpl.ma

diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
new file mode 100644
index 000000000..887566f58
--- /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).
-- 
2.39.2