diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 38fc68c56..b5bb77c19 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1199,7 +1199,6 @@ struct unifier_fn {
     */
     void mk_simple_nonlocal_projection(expr const & m, buffer<expr> const & margs, unsigned i, expr const & rhs, justification const & j,
                               buffer<constraints> & alts) {
-        lean_assert(!is_local(rhs));
         expr const & mtype = mlocal_type(m);
         unsigned vidx = margs.size() - i - 1;
         expr const & marg = margs[i];