let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in
mk_pred metasenv subst (hyp :: context') pred arg' cpattern' tail
in
let metasenv, subst, pred, arg =
mk_pred metasenv subst context goal arg cpattern (List.rev actual_args)
in
let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in
mk_pred metasenv subst (hyp :: context') pred arg' cpattern' tail
in
let metasenv, subst, pred, arg =
mk_pred metasenv subst context goal arg cpattern (List.rev actual_args)
in