match CicReduction.whd ~subst context te with
C.Rel m when List.mem m safes -> true
| C.Rel _
- | C.Appl _
| C.MutConstruct _
| C.Const _
| C.Var _ -> false
+ | C.Appl (he::_) ->
+ check_is_really_smaller_arg rec_uri rec_uri_len
+ ~logger ~metasenv ~subst context n nn kl x safes he
| C.Lambda (name,ty,ta) ->
check_is_really_smaller_arg rec_uri rec_uri_len
~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context)