| nplus_succ_2: \forall q, r. NPlus p q r \to NPlus p (succ q) (succ r).
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural plus (relational)" 'rel_plus x y z =
+interpretation "natural plus predicate" 'rel_plus x y z =
(cic:/matita/RELATIONAL/NPlus/defs/NPlus.ind#xpointer(1/1) x y z).
notation "hvbox(a break + b break == c)"