3 match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
6 | (S x) \Rightarrow false ]
8 [\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
9 match (le_n O): le with
10 [ le_n \Rightarrow (refl_equal nat O)
11 | (le_S x y) \Rightarrow (refl_equal nat O) ]
14 [\lambda z:nat. \lambda h:(le 1 z). (le 0 z)]
15 match (le_S 2 (le_n 1)): le with
16 [ le_n \Rightarrow (le_S 1 (le_n 0))
17 | (le_S x y) \Rightarrow y ]
20 [\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
21 match (le_S 0 0 (le_n 0)): le with
22 [ le_n \Rightarrow (le_S 0 0 (le_n 0))
23 | (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
28 | false \Rightarrow (S O) ]
33 | (S x) \Rightarrow (S (S x)) ]
35 [\lambda x:list. list]
38 | (cons x y) \Rightarrow (cons x y) ]
41 [\lambda h:False. True]