(* 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 *)
(* 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 *)