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