+let default_eq_URIs =
+ [HelmLibraryObjects.Logic.eq_URI,
+ HelmLibraryObjects.Logic.sym_eq_URI,
+ HelmLibraryObjects.Logic.trans_eq_URI,
+ HelmLibraryObjects.Logic.eq_ind_URI,
+ HelmLibraryObjects.Logic.eq_ind_r_URI];;
+
+let default_true_URIs = [HelmLibraryObjects.Logic.true_URI]
+let default_false_URIs = [HelmLibraryObjects.Logic.false_URI]
+let default_absurd_URIs = [HelmLibraryObjects.Logic.absurd_URI]
+