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)((le O n)->(eq nat n n))](f O (le_n O))
6 ### (* TYPE_OF the disambiguated term *)
7 (f:(n:nat)((le O n)->(eq nat n n)))(eq nat O O)
8 ### (* REDUCED disambiguated term *)
9 [f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O))