1 inductive pos: Set \def
9 inductive int: Set \def
10 | positive: nat \to int
11 | negative : nat \to int.
13 inductive empty : Set \def .
15 let rec pos2nat x \def
17 [ one \Rightarrow (S O)
18 | (next z) \Rightarrow S (pos2nat z)].
20 definition nat2int \def \lambda x. positive x.
26 definition fst \def \lambda x,y:int.x.
27 alias symbol "eq" (instance 0) = "leibnitz's equality".
29 theorem a: fst O one = fst (positive O) (next one).