(\lambda f. (f 0 (le_n 0))
  \lambda n. \lambda H. (refl_equal nat 0)))