helm/gTopLevel/tests/forall00.cic.test

   1 \forall n:nat. \forall m. n + m = n
   2 ###### INTERPRETATION NUMBER 1 ######
   3 ### (* disambiguation environment  *)
   4 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
   5 alias symbol "eq" (instance 0) = "leibnitz's equality"
   6 alias symbol "plus" (instance 0) = "natural plus"
   7 ### (* METASENV after disambiguation  *)
   8
   9 ### (* TERM after disambiguation      *)
  10 (n:nat)(m:nat)(eq nat (plus n m) n)
  11 ### (* TYPE_OF the disambiguated term *)
  12 Prop
  13 ### (* REDUCED disambiguated term     *)
  14 (n:nat)(m:nat)(eq nat (plus n m) n)