helm/gTopLevel/tests/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)(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))