--- /dev/null
+[nat]
+match true:bool with
+[ true \Rightarrow O
+| false \Rightarrow (S O)
+]
+
+[nat]
+match O:nat with
+[ O \Rightarrow O
+| (S x) \Rightarrow (S (S x))
+]
+
+[nat]
+match nil:list with
+[ nil \Rightarrow nil
+| (cons x y) \Rightarrow (cons x y)
+]
+