1 set "baseuri" "cic:/matita/tests/coercions/".
3 inductive pos: Set \def
11 inductive int: Set \def
12 | positive: nat \to int
13 | negative : nat \to int.
15 inductive empty : Set \def .
17 let rec pos2nat x \def
19 [ one \Rightarrow (S O)
20 | (next z) \Rightarrow S (pos2nat z)].
22 definition nat2int \def \lambda x. positive x.
28 definition fst \def \lambda x,y:int.x.
29 alias symbol "eq" (instance 0) = "leibnitz's equality".
31 theorem a: fst O one = fst (positive O) (next one).