Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
type_of_rc;
pack_coercion_obj: Cic.obj -> Cic.obj;
apply_subst: Cic.substitution -> Cic.term -> Cic.term ;
Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
type_of_rc;
pack_coercion_obj: Cic.obj -> Cic.obj;
apply_subst: Cic.substitution -> Cic.term -> Cic.term ;