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