| 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 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