+set "baseuri" "cic:/matita/tests/coercions/".
+
inductive pos: Set \def
| one : pos
| next : pos \to pos.
coercion nat2int.
definition fst \def \lambda x,y:int.x.
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
theorem a: fst O one = fst (positive O) (next one).
reflexivity.