inductive eq (A:Type) (x:A) : A \to Prop \def
refl_eq : eq A x x.
+(*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".