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)(nat->(eq nat (plus n __1) n))
   6 ### (* TYPE_OF the disambiguated term *)
   7 Prop
   8 ### (* REDUCED disambiguated term     *)
   9 (n:nat)(nat->(eq nat (plus n __1) n))