test_instance.ma

diff --git a/helm/matita/tests/test_instance.ma b/helm/matita/tests/test_instance.ma
new file mode 100644 (file)
index 0000000..cb3aa3f
--- /dev/null
+++ b/helm/matita/tests/test_instance.ma
@@ -0,0 +1,4 @@
+instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x.
+instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x.
+instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z.
+instance \lambda A:Set.\lambda f:A \to A \to A. \forall x,y:A. f x y = f  y x.
\ No newline at end of file