(*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)).
theorem reflexive_eq : \forall A:Type. reflexive A (eq A).
simplify.intros.apply refl_eq.