(* since it needs to restrict the metavariables in case of failure *)
val lift : int -> Cic.term -> Cic.term
-
(* lift from n t *)
(* as lift but lifts only indexes >= from *)
val lift_from: int -> int -> Cic.term -> Cic.term
+(* lift map t *)
+(* as lift_from but lifts indexes by applying a map to them
+ the first argument of the map is the current depth *)
+(* FG: this is used in CicDischarge to perform non-linear relocation *)
+val lift_map: int -> (int -> int -> int) -> Cic.term -> Cic.term
+
(* subst t1 t2 *)
(* substitutes [t1] for [Rel 1] in [t2] *)
(* if avoid_beta_redexes is true (default: false) no new beta redexes *)