val lift : int -> Cic.term -> Cic.term
val subst : Cic.term -> Cic.term -> Cic.term
val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term
-val delift :
- Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj