+(*
+coercion cic:/matita/logic/equality/sym_eq.con.
+coercion cic:/matita/logic/equality/eq_f.con.
+*)
+
+default "equality"
+ cic:/matita/logic/equality/eq.ind
+ cic:/matita/logic/equality/sym_eq.con
+ cic:/matita/logic/equality/trans_eq.con
+ cic:/matita/logic/equality/eq_ind.con
+ cic:/matita/logic/equality/eq_elim_r.con
+ cic:/matita/logic/equality/eq_f.con
+ cic:/matita/logic/equality/eq_f'.con. (* \x.sym (eq_f x) *)
+