+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "leibnitz's equality"
+ 'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "leibnitz's non-equality"
+ 'neq x y = (cic:/matita/logic/connectives/Not.con
+ (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)).
+