(* collapse non-indexable terms, not removing coercions *)
val key: Cic.term -> Cic.term
+val in_universe: universe -> Cic.term -> Cic.term option
+
(* indexes the term and its unfolded both without coercions *)
val index_term_and_unfolded_term:
universe -> Cic.context -> Cic.term -> Cic.term -> universe