diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index c409a91c45..47e4f9c5c8 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2141,7 +2141,23 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
             optional<metavar_decl> m2_decl = m_mctx.get_metavar_decl(f2);
             if (m1_decl && m2_decl) {
                 if (m2_decl->get_context().is_subset_of(m1_decl->get_context())) {
-                    return to_lbool(process_assignment(e1, e2));
+                    if (!is_app(e1) || is_app(e2)) {
+                        return to_lbool(process_assignment(e1, e2));
+                    } else if (m1_decl->get_context().is_subset_of(m2_decl->get_context())) {
+                        lean_assert(is_app(e1) && !is_app(e2));
+                        /* It is easier to solve the assignment
+                                 ?m2 := ?m1 a_1 ... a_n
+                           than
+                                 ?m1 a_1 ... a_n := ?m2
+                           Reason: the first one is precise. For example,
+                           consider the following constraint:
+
+                                 ?m1 ?m =?= ?m2
+                        */
+                        return to_lbool(process_assignment(e2, e1));
+                    } else {
+                        return to_lbool(process_assignment(e1, e2));
+                    }
                 } else {
                     return to_lbool(process_assignment(e2, e1));
                 }