- | NCic.Meta (_,(m,_)) as t when m >= k + nargs - 1 -> t
- | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
+ | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 ->
+ if delift then NCic.Meta (i,(m-nargs,l)) else t
+ | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m ->
+ if delift then NCic.Meta (i,(m-nargs,irl)) else t