(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)
(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)