| NCic.Meta _ -> metasenv, subst
| NCic.Implicit _ -> metasenv, subst
| NCic.Appl (NCic.Rel i :: args) as t
- when i >= List.length context - len ->
+ when i > List.length context - len ->
let lefts, _ = HExtlib.split_nth leftno args in
let ctxlen = List.length context in
let (metasenv, subst), _ =