[ le_n \Rightarrow (refl_equal nat O)
| (le_S x y) \Rightarrow (refl_equal nat O) ]
+[\lambda z:nat. \lambda h:(le (plus (plus O O) (plus O O)) z). (eq nat (plus (plus O O) (plus O O)) (plus (plus O O) (plus O O)))]
+match (le_n (plus (plus O O) (plus O O))): le with
+[ le_n \Rightarrow (refl_equal nat (plus (plus O O) (plus O O)))
+| (le_S x y) \Rightarrow (refl_equal nat (plus (plus O O) (plus O 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 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
[ nil \Rightarrow nil
| (cons x y) \Rightarrow (cons x y) ]
+\lambda x:False.
+ [\lambda h:False. True]
+ match x:False with []
+