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