+
+(*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: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+