| C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
| _ when i > 0 -> true
| _ -> false
+
+let lift k n =
+ let rec lift_xns k (uri, t) = uri, lift_term k t
+ and lift_ms k = function
+ | None -> None
+ | Some t -> Some (lift_term k t)
+ and lift_fix len k (id, name, i, ty, bo) =
+ id, name, i, lift_term k ty, lift_term (k + len) bo
+ and lift_cofix len k (id, name, ty, bo) =
+ id, name, lift_term k ty, lift_term (k + len) bo
+ and lift_term k = function
+ | C.ASort _ as t -> t
+ | C.AImplicit _ as t -> t
+ | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b)
+ | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss)
+ | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss)
+ | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss)
+ | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss)
+ | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss)
+ | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts)
+ | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty)
+ | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
+ | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
+ | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
+ | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t)
+ | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
+ | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
+ in
+ lift_term k