[\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 ]

[\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
match (le_n O): le with
[ le_n \Rightarrow (refl_equal nat O)
| (le_S x y) \Rightarrow (refl_equal nat O) ]

(*
[\lambda z:nat. \lambda h:(le 1 z). (le 0 z)]
match (le_S 2 (le_n 1)): le with
[ le_n \Rightarrow (le_S 1 (le_n 0))
| (le_S x y) \Rightarrow y ]
*)

[\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
match (le_S 0 0 (le_n 0)): le with
[ le_n \Rightarrow (le_S 0 0 (le_n 0))
| (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]

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

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

[\lambda x:list. list]
match nil:list with
[ nil \Rightarrow nil
| (cons x y) \Rightarrow (cons x y) ]

\lambda x:False.
  [\lambda h:False. True]
  match x:False with []