+
+val is_in: equality_bag -> int -> bool
+
+(* symmetric [eq_ty] [l] [id] [uri] [m]
+ *
+ * given an equality (_,p,(_,[l],r,_),[m],[id]) of 'type' l=r
+ * returns the proof of the symmetric (r=l).
+ *
+ * [uri] is the uri of eq
+ * [eq_ty] the ty of the equality sides
+ *)
+val symmetric:
+ equality_bag -> Cic.term -> Cic.term -> int -> UriManager.uri ->
+ Cic.metasenv -> equality_bag * proof
+
+(* takes 3 lists of alive ids (they are threated the same way, the type is
+ * funny just to not oblige you to concatenate them) and drops all the dead
+ * equalities *)
+val collect: equality_bag -> int list -> int list -> int list -> equality_bag
+
+(* given an equality, returns the numerical id *)
+val id_of: equality -> int
+
+(* profiling statistics *)
+val get_stats: unit -> string
+