1 \lambda f:(\forall n:nat. (\forall H:(le 0 n). (n=n))). (f 0 (le_n 0))
2 ### (* METASENV after disambiguation *)
4 ### (* TERM after disambiguation *)
5 [f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O))
6 ### (* TYPE_OF the disambiguated term *)
7 (f:(n:nat)(H:(le O n))(eq nat n n))(eq nat O O)
8 ### (* REDUCED disambiguated term *)
9 [f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O))