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