fix

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

diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma
new file mode 100644 (file)
index 0000000..9e86635
--- /dev/null
+++ b/helm/matita/tests/apply.ma
@@ -0,0 +1,24 @@
+%% test _with_ the WHD on the apply argument
+
+alias id "not" = "cic:/Coq/Init/Logic/not.con".
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+
+theorem b:
+  \forall x:Prop.
+  (not x) \to x \to False.
+intro.
+apply H.
+assumption.
+qed.
+
+%% test _without_ the WHD on the apply argument
+
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+
+theorem a:
+  \forall A:Set.
+  \forall x,y : A.
+  not (x=y) \to not (x=y).
+intro.
+apply H.
+qed.