(**************************************************************************)
set "baseuri" "cic:/matita/tests/cut".
-include "coq.ma".
+include "legacy/coq.ma".
alias num (instance 0) = "natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
theorem stupid: 3 = 3.
- cut 3 = 3.
+ cut (3 = 3).
assumption.
reflexivity.
- qed.
+qed.