(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)
(* it returns the list of the uris of the auxiliary lemmas generated *)
val add_obj:
RefinementTool.kit ->
(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)
(* it returns the list of the uris of the auxiliary lemmas generated *)
val add_obj:
RefinementTool.kit ->