let lift_from k n =
let rec liftaux k = function
| C.Rel m as t -> if m < k then t else C.Rel (m + n)
+ | C.Meta (i,(m,(C.Irl 0 as l))) when k <= m+1 -> C.Meta (i,(m,l))
| 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)) ->