| C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l))
| C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
| C.Meta (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
C.Meta (i, (m, C.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx)))
| C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l))
| C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
| C.Meta (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
C.Meta (i, (m, C.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx)))