[\lambda x:nat. nat]
match O:nat with
[ O \Rightarrow O
| (S x) \Rightarrow (S (S x)) ]