lambda02.cic.test

   1 \lambda f:(\forall n:nat. (\forall H:(le 0 n). (n=n))). (f 0 (le_n 0))
   2 ### (* METASENV after disambiguation  *)
   3
   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))