helm/gTopLevel/tests/forall00.cic.test

   1 \forall n:nat. \forall m. n + m = n
   2 ### (* METASENV after disambiguation  *)
   3
   4 ### (* TERM after disambiguation      *)
   5 (n:nat)(m:nat)(eq nat (plus n m) n)
   6 ### (* TYPE_OF the disambiguated term *)
   7 Prop
   8 ### (* REDUCED disambiguated term     *)
   9 (n:nat)(m:nat)(eq nat (plus n m) n)