+(* *)
+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/transitive_eq.con
+ cic:/matita/logic/equality/eq_ind.con
+ cic:/matita/logic/equality/eq_elim_r.con
+ cic:/matita/logic/equality/eq_rec.con
+ cic:/matita/logic/equality/eq_elim_r'.con
+ cic:/matita/logic/equality/eq_rect.con
+ cic:/matita/logic/equality/eq_elim_r''.con
+ cic:/matita/logic/equality/eq_f.con
+(* *)
+ cic:/matita/logic/equality/eq_OF_eq.con.
+(* *)
+(*
+ cic:/matita/logic/equality/eq_f'.con. (* \x.sym (eq_f x) *)
+ *)
+