"equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;eq_ind_r_URI] ->
eq_URIs_ref :=
insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI)
"equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;eq_ind_r_URI] ->
eq_URIs_ref :=
insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI)