\forall n:nat. \forall m. n + m = n
###### INTERPRETATION NUMBER 1 ######
### (* disambiguation environment *)
-alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
+alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
alias symbol "eq" (instance 0) = "leibnitz's equality"
alias symbol "plus" (instance 0) = "natural plus"
### (* METASENV after disambiguation *)