### (* METASENV after disambiguation *)
### (* TERM after disambiguation *)
-(n:nat)(nat->(eq nat (plus n __1) n))
+(n:nat)(m:nat)(eq nat (plus n m) n)
### (* TYPE_OF the disambiguated term *)
Prop
### (* REDUCED disambiguated term *)
-(n:nat)(nat->(eq nat (plus n __1) n))
+(n:nat)(m:nat)(eq nat (plus n m) n)