(*CSC: the URI must disappear: there is a bug now *)
interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y).