(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/logic/equality/".
-
include "higher_order_defs/relations.ma".
inductive eq (A:Type) (x:A) : A \to Prop \def
qed.
(* *)
-coercion cic:/matita/logic/equality/sym_eq.con.
-coercion cic:/matita/logic/equality/eq_f.con.
+coercion sym_eq.
+coercion eq_f.
(* *)
default "equality"