if delift && nargs <> 0 then NCic.Rel (n - nargs) else t
| n when n < k -> t
| n (* k <= n < k+nargs *) ->
- (try lift (k+lift_args) (map_arg (List.nth args (n-k)))
+ (try lift (k-1+lift_args) (map_arg (List.nth args (n-k)))
with Failure _ -> assert false))
| NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 ->
if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t