]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/tests/forall00.cic.test
sort_of_prod relaxed to accept also Metas (when the second Meta has an
[helm.git] / 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)