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 let rec nat2int x \def
22 [ O \Rightarrow positive O
23 | (S z) \Rightarrow positive (S z)].
31 [ (positive n) \Rightarrow x
32 | (negative z) \Rightarrow y].
34 theorem a: plus O one.