let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
let add_to_universe (universe,status) uri =
let term = CicUtil.term_of_uri uri in
let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
let add_to_universe (universe,status) uri =
let term = CicUtil.term_of_uri uri in