| C.Rel m when List.mem m safes -> true
| C.Lambda (name, s, t) ->
is_really_smaller ~subst ~metasenv (shift_k (name, C.Decl s) k) t
- | C.Rel _
+ | C.Appl (he::_) ->
+ is_really_smaller ~subst ~metasenv k he
| C.Appl _
+ | C.Rel _
| C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
| C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
(*| C.Fix (_, fl) ->