| 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.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)