(* lifts [t] of [n] *)
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
+
(* subst t1 t2 *)
(* substitutes [t1] for [Rel 1] in [t2] *)
val subst : Cic.term -> Cic.term -> Cic.term