(*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).
+ 'eq t x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t 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)).
+ 'neq t x y = (cic:/matita/logic/connectives/Not.con
+ (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y)).
theorem eq_rect':
\forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type.