]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/tests/cut.ma
fix
[helm.git] / helm / matita / tests / cut.ma
index 8ba63bd8b9959898f28d98a4fbbf2f17c96915db..82d36667b6d6daffa900f638eb3d856530a02cb5 100644 (file)
@@ -16,8 +16,8 @@ set "baseuri" "cic:/matita/tests/cut".
 alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "leibnitz's equality".
 
-theorem stupid: 0 = 0.
-  cut 0 = 0.
+theorem stupid: 3 = 3.
+  cut 3 = 3.
   assumption.
   reflexivity.
   qed.