+++ /dev/null
-set "baseuri" "cic:/matita/tests/drop".
-
-alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
-alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "plus" (instance 0) = "natural plus".
-theorem a : O + 1 = 1.
-drop.