diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index ea678aeb28..54a5c5ccf6 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -86,7 +86,7 @@ environment check_cmd(parser & p) {
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     level_param_names new_ls;
     std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
-    auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen());
+    auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen(), true);
     expr type = tc->check(e, append(ls, new_ls));
     auto reg              = p.regular_stream();
     formatter const & fmt = reg.get_formatter();
@@ -270,7 +270,7 @@ environment opaque_hint_cmd(parser & p) {
             if (p.curr_is_token(g_module)) {
                 found = true;
                 p.next();
-                env = set_main_module_opaque_defs(env, hiding);
+                env = set_hide_main_opaque(env, hiding);
             } else {
                 name c  = p.check_constant_next("invalid 'opaque_hint', constant expected");
                 found   = true;
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 09daad7a5b..a5f464a63d 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -271,11 +271,11 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
             std::tie(type, new_ls) = p.elaborate_type(type);
             env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
         } else {
-            std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
+            std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
             env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
         }
     } else {
-        std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
+        std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
         env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque)));
     }
     if (real_n != n)
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 9314f7066e..2a626a7769 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -131,7 +131,7 @@ class elaborator {
     local_decls<level>  m_lls;
     io_state            m_ios;
     name_generator      m_ngen;
-    type_checker_ptr    m_tc;
+    type_checker_ptr    m_tc[2];
     substitution        m_subst;
     expr_map<expr>      m_cache; // (pointer equality) cache for Type and Constants (this is a trick to make sure we get the
                                  // same universe metavariable for different occurrences of the same Type/Constant
@@ -148,6 +148,7 @@ class elaborator {
     name_set            m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
     bool                m_check_unassigned; // if true if display error messages if elaborated term still contains metavariables
     bool                m_use_local_instances; // if true class-instance resolution will use the local context
+    bool                m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent
 
     // Set m_ctx to ctx, and make sure m_ctx_buffer and m_ctx_domain_buffer reflect the contents of the new ctx
     void set_ctx(context const & ctx) {
@@ -173,12 +174,14 @@ class elaborator {
             lean_assert(m_main.m_accumulated.is_none());
             m_old_ctx    = m_main.m_ctx;
             m_main.set_ctx(ctx);
-            m_main.m_tc->push();
+            m_main.m_tc[0]->push();
+            m_main.m_tc[1]->push();
             m_main.m_subst = s;
         }
         ~scope() {
             m_main.set_ctx(m_old_ctx);
-            m_main.m_tc->pop();
+            m_main.m_tc[0]->pop();
+            m_main.m_tc[1]->pop();
             m_main.m_constraints.clear();
             m_main.m_accumulated = justification();
             m_main.m_subst = substitution();
@@ -189,8 +192,9 @@ class elaborator {
 
     /* \brief Move all constraints generated by the type checker to the buffer m_constraints. */
     void consume_tc_cnstrs() {
-        while (auto c = m_tc->next_cnstr())
-            m_constraints.push_back(*c);
+        for (unsigned i = 0; i < 2; i++)
+            while (auto c = m_tc[i]->next_cnstr())
+                m_constraints.push_back(*c);
     }
 
     struct choice_elaborator {
@@ -212,8 +216,9 @@ class elaborator {
         context      m_ctx;
         substitution m_subst;
         unsigned     m_idx;
-        choice_expr_elaborator(elaborator & elab, expr const & mvar, expr const & c, context const & ctx, substitution const & s):
-            m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_subst(s), m_idx(0) {
+        bool         m_relax_main_opaque;
+        choice_expr_elaborator(elaborator & elab, expr const & mvar, expr const & c, context const & ctx, substitution const & s, bool relax):
+            m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_subst(s), m_idx(0), m_relax_main_opaque(relax) {
         }
 
         virtual optional<constraints> next() {
@@ -226,7 +231,7 @@ class elaborator {
                     justification j = m_elab.m_accumulated;
                     m_elab.consume_tc_cnstrs();
                     list<constraint> cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end());
-                    cs = cons(mk_eq_cnstr(m_mvar, r, j), cs);
+                    cs = cons(mk_eq_cnstr(m_mvar, r, j, m_relax_main_opaque), cs);
                     return optional<constraints>(cs);
                 } catch (exception &) {}
             }
@@ -263,13 +268,14 @@ class elaborator {
         context                 m_ctx; // local context for m_meta
         substitution            m_subst;
         justification           m_jst;
+        bool                    m_relax_main_opaque;
 
         placeholder_elaborator(elaborator & elab, expr const & meta, expr const & meta_type,
                                list<expr> const & local_insts, list<name> const & instances, list<tactic_hint_entry> const & tacs,
-                               context const & ctx, substitution const & s, justification const & j, bool ignore_failure):
+                               context const & ctx, substitution const & s, justification const & j, bool ignore_failure, bool relax):
             choice_elaborator(ignore_failure),
             m_elab(elab), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances),
-            m_tactics(tacs), m_ctx(ctx), m_subst(s), m_jst(j) {
+            m_tactics(tacs), m_ctx(ctx), m_subst(s), m_jst(j), m_relax_main_opaque(relax) {
             collect_metavars(meta_type, m_mvars_in_meta_type);
         }
 
@@ -292,7 +298,7 @@ class elaborator {
                 for (auto & c : m_elab.m_constraints)
                     c = update_justification(c, mk_composite1(m_jst, c.get_justification()));
                 list<constraint> cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end());
-                cs = cons(mk_eq_cnstr(m_meta, r, mk_composite1(m_jst, j)), cs);
+                cs = cons(mk_eq_cnstr(m_meta, r, mk_composite1(m_jst, j), m_relax_main_opaque), cs);
                 return optional<constraints>(cs);
             } catch (exception &) {
                 return optional<constraints>();
@@ -307,9 +313,9 @@ class elaborator {
                 substitution subst = next->first.get_subst();
                 buffer<constraint> cs;
                 expr const & mvar = get_app_fn(m_meta);
-                cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst));
+                cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, m_relax_main_opaque));
                 for (auto const & mvar : m_mvars_in_meta_type)
-                    cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst));
+                    cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, m_relax_main_opaque));
                 return optional<constraints>(to_list(cs.begin(), cs.end()));
             }
             return optional<constraints>();
@@ -319,7 +325,7 @@ class elaborator {
             while (!empty(m_local_instances)) {
                 expr inst         = head(m_local_instances);
                 m_local_instances = tail(m_local_instances);
-                constraints cs(mk_eq_cnstr(m_meta, inst, m_jst));
+                constraints cs(mk_eq_cnstr(m_meta, inst, m_jst, m_relax_main_opaque));
                 return optional<constraints>(cs);
             }
             while (!empty(m_instances)) {
@@ -362,8 +368,11 @@ public:
     elaborator(environment const & env, local_decls<level> const & lls, list<expr> const & ctx, io_state const & ios, name_generator const & ngen,
                pos_info_provider * pp, bool check_unassigned):
         m_env(env), m_lls(lls), m_ios(ios),
-        m_ngen(ngen), m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())),
+        m_ngen(ngen),
         m_pos_provider(pp) {
+        m_relax_main_opaque = false;
+        m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false);
+        m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true);
         m_check_unassigned = check_unassigned;
         m_use_local_instances = get_elaborator_local_instances(ios.get_options());
         set_ctx(ctx);
@@ -375,10 +384,11 @@ public:
 
     expr infer_type(expr const & e) {
         lean_assert(closed(e));
-        return m_tc->infer(e); }
+        return m_tc[m_relax_main_opaque]->infer(e);
+    }
 
     expr whnf(expr const & e) {
-        return m_tc->whnf(e);
+        return m_tc[m_relax_main_opaque]->whnf(e);
     }
 
     /** \brief Clear constraint buffer \c m_constraints, and associated datastructures
@@ -593,7 +603,7 @@ public:
                     return lazy_list<constraints>(); // nothing to be done
                 bool ignore_failure = false; // we are always strict with placeholders associated with classes
                 return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, local_insts, insts, tacs, ctx, s, j,
-                                                                       ignore_failure));
+                                                                       ignore_failure, m_relax_main_opaque));
             } else if (s.is_assigned(mvar)) {
                 // if the metavariable is assigned and it is not a class, then we just ignore it, and return
                 // the an empty set of constraints.
@@ -602,10 +612,10 @@ public:
                 list<tactic_hint_entry> tacs = get_tactic_hints(m_env);
                 bool ignore_failure = !is_strict;
                 return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, list<expr>(), list<name>(), tacs, ctx, s, j,
-                                                                       ignore_failure));
+                                                                       ignore_failure, m_relax_main_opaque));
             }
         };
-        add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j));
+        add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j, m_relax_main_opaque));
         return m;
     }
 
@@ -642,11 +652,12 @@ public:
         // Possible optimization: try to lookahead and discard some of the alternatives.
         expr m      = mk_meta(t, e.get_tag());
         context ctx = m_ctx;
+        bool relax = m_relax_main_opaque;
         auto fn = [=](expr const & mvar, expr const & /* type */, substitution const & s, name_generator const & /* ngen */) {
-            return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, ctx, s));
+            return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, ctx, s, relax));
         };
         justification j = mk_justification("none of the overloads is applicable", some_expr(e));
-        add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j));
+        add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j, m_relax_main_opaque));
         return m;
     }
 
@@ -670,7 +681,7 @@ public:
             f_type = whnf(instantiate_metavars(f_type));
             if (!is_pi(f_type) && is_meta(f_type)) {
                 // let type checker add constraint
-                f_type = m_tc->ensure_pi(f_type, f);
+                f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f);
             }
         }
         if (!is_pi(f_type)) {
@@ -710,6 +721,7 @@ public:
     }
 
     constraint mk_delayed_coercion_cnstr(expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor) {
+        bool relax = m_relax_main_opaque;
         auto choice_fn = [=](expr const & mvar, expr const & new_d_type, substitution const & /* s */, name_generator const & /* ngen */) {
             // Remark: we want the coercions solved before we start discarding FlexFlex constraints. So, we use PreFlexFlex as a max cap
             // for delaying coercions.
@@ -718,10 +730,10 @@ public:
                 return lazy_list<constraints>(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(), delay_factor+1)));
             } else {
                 expr r = apply_coercion(a, a_type, new_d_type);
-                return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification())));
+                return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification(), relax)));
             }
         };
-        return mk_choice_cnstr(m, choice_fn, delay_factor, j);
+        return mk_choice_cnstr(m, choice_fn, delay_factor, j, m_relax_main_opaque);
     }
 
     /** \brief Given an application \c e, where the expected type is d_type, and the argument type is a_type,
@@ -792,19 +804,19 @@ public:
             return mk_delayed_coercion(r, d_type, a_type);
         } else {
             app_delayed_justification j(r, f_type, a_type);
-            if (!m_tc->is_def_eq(a_type, d_type, j)) {
+            if (!m_tc[m_relax_main_opaque]->is_def_eq(a_type, d_type, j)) {
                 expr new_a = apply_coercion(a, a_type, d_type);
                 bool coercion_worked = false;
                 if (!is_eqp(a, new_a)) {
                     expr new_a_type = instantiate_metavars(infer_type(new_a));
-                    coercion_worked = m_tc->is_def_eq(new_a_type, d_type, j);
+                    coercion_worked = m_tc[m_relax_main_opaque]->is_def_eq(new_a_type, d_type, j);
                 }
                 if (coercion_worked) {
                     r = update_app(r, f, new_a);
                 } else {
                     if (has_metavar(a_type) || has_metavar(d_type)) {
                         // rely on unification hints to solve this constraint
-                        add_cnstr(mk_eq_cnstr(a_type, d_type, j.get()));
+                        add_cnstr(mk_eq_cnstr(a_type, d_type, j.get(), m_relax_main_opaque));
                     } else {
                         throw_kernel_exception(m_env, r, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, d_type, a_type); });
                     }
@@ -888,7 +900,7 @@ public:
                 return e;
             if (is_meta(t)) {
                 // let type checker add constraint
-                m_tc->ensure_sort(t, e);
+                m_tc[m_relax_main_opaque]->ensure_sort(t, e);
                 return e;
             }
         }
@@ -1112,7 +1124,7 @@ public:
             if (!meta)
                 return;
             meta = instantiate_meta(*meta, subst);
-            expr type = m_tc->infer(*meta);
+            expr type = m_tc[m_relax_main_opaque]->infer(*meta);
             // first solve unassigned metavariables in type
             type = solve_unassigned_mvars(subst, type, visited);
             proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
@@ -1173,7 +1185,8 @@ public:
         return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
     }
 
-    std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type) {
+    std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) {
+        flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(m_env));
         expr r  = visit(e);
         if (_ensure_type)
             r = ensure_type(r);
@@ -1183,16 +1196,18 @@ public:
         return apply(s, r);
     }
 
-    std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n) {
+    std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque) {
         lean_assert(!has_local(t)); lean_assert(!has_local(v));
         expr r_t      = ensure_type(visit(t));
+        // Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent.
+        flet<bool> set_relax(m_relax_main_opaque, is_opaque && !get_hide_main_opaque(m_env));
         expr r_v      = visit(v);
         expr r_v_type = infer_type(r_v);
         justification j = mk_justification(v, [=](formatter const & fmt, substitution const & subst) {
                 substitution s(subst);
                 return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
             });
-        if (!m_tc->is_def_eq(r_v_type, r_t, j)) {
+        if (!m_tc[is_opaque]->is_def_eq(r_v_type, r_t, j)) {
             throw_kernel_exception(m_env, v, [=](formatter const & fmt) { return pp_def_type_mismatch(fmt, n, r_t, r_v_type); });
         }
         auto p  = solve().pull();
@@ -1209,13 +1224,13 @@ public:
 static name g_tmp_prefix = name::mk_internal_unique_name();
 
 std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
-                                              io_state const & ios, expr const & e, pos_info_provider * pp, bool check_unassigned,
-                                              bool ensure_type) {
-    return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type);
+                                              io_state const & ios, expr const & e, bool relax_main_opaque,
+                                              pos_info_provider * pp, bool check_unassigned, bool ensure_type) {
+    return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type, relax_main_opaque);
 }
 
 std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
-                                                    name const & n, expr const & t, expr const & v, pos_info_provider * pp) {
-    return elaborator(env, lls, list<expr>(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n);
+                                                    name const & n, expr const & t, expr const & v, bool is_opaque, pos_info_provider * pp) {
+    return elaborator(env, lls, list<expr>(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n, is_opaque);
 }
 }
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 5cd9155fa9..128853e3b6 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -14,9 +14,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
-                                              io_state const & ios, expr const & e, pos_info_provider * pp = nullptr,
-                                              bool check_unassigned = true, bool ensure_type = false);
+                                              io_state const & ios, expr const & e, bool relax_main_opaque,
+                                              pos_info_provider * pp = nullptr, bool check_unassigned = true, bool ensure_type = false);
 std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls,
                                                     io_state const & ios, name const & n, expr const & t, expr const & v,
-                                                    pos_info_provider * pp = nullptr);
+                                                    bool is_opaque, pos_info_provider * pp = nullptr);
 }
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 955bbbf9cf..80e9d67b6b 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -90,7 +90,7 @@ struct inductive_cmd_fn {
         m_u = mk_global_univ(u_name);
         m_infer_result_universe = false;
         m_namespace = get_namespace(m_env);
-        m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen());
+        m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen(), false);
     }
 
     [[ noreturn ]] void throw_error(char const * error_msg) { throw parser_error(error_msg, m_pos); }
@@ -402,7 +402,7 @@ struct inductive_cmd_fn {
             std::tie(d_name, d_type, std::ignore) = d;
             m_env = m_env.add(check(m_env, mk_var_decl(d_name, ls, d_type)));
         }
-        m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen());
+        m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen(), false);
     }
 
     /** \brief Traverse the introduction rule type and collect the universes where non-parameters reside in \c r_lvls.
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index b2bb1341f6..211ca5abc7 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -485,28 +485,34 @@ level parser::parse_level(unsigned rbp) {
 
 std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> const & ctx) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, &pp, false);
+    bool relax            = true;
+    bool check_unassigned = false;
+    return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned);
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, &pp, true, true);
+    bool relax            = false;
+    bool ensure_type      = true;
+    bool check_unassigned = true;
+    return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type);
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(env, m_local_level_decls, list<expr>(), m_ios, e, &pp);
+    bool relax            = false;
+    return ::lean::elaborate(env, m_local_level_decls, list<expr>(), m_ios, e, relax, &pp);
 }
 
-std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v) {
+std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp);
+    return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, is_opaque, &pp);
 }
 
 std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
-                                                                          name const & n, expr const & t, expr const & v) {
+                                                                          name const & n, expr const & t, expr const & v, bool is_opaque) {
     parser_pos_provider pp = get_pos_provider();
-    return ::lean::elaborate(env, lls, m_ios, n, t, v, &pp);
+    return ::lean::elaborate(env, lls, m_ios, n, t, v, is_opaque, &pp);
 }
 
 [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 861aacc00d..d7ab996db2 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -262,9 +262,10 @@ public:
     /** \brief Elaborate \c e (making sure the result does not have metavariables). */
     std::tuple<expr, level_param_names> elaborate(expr const & e) { return elaborate_at(m_env, e); }
     /** \brief Elaborate the definition n : t := v */
-    std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
+    std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque);
     /** \brief Elaborate the definition n : t := v in the given environment*/
-    std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls, name const & n, expr const & t, expr const & v);
+    std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls,
+                                                                      name const & n, expr const & t, expr const & v, bool is_opaque);
 
     parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); }
 
diff --git a/src/frontends/lean/theorem_queue.cpp b/src/frontends/lean/theorem_queue.cpp
index b0e0e37e71..08c3fff919 100644
--- a/src/frontends/lean/theorem_queue.cpp
+++ b/src/frontends/lean/theorem_queue.cpp
@@ -16,7 +16,8 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam
     m_queue.add([=]() {
             level_param_names new_ls;
             expr type, value;
-            std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v);
+            bool is_opaque = true; // theorems are always opaque
+            std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v, is_opaque);
             return check(env, mk_theorem(n, append(ls, new_ls), type, value));
         });
 }
diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp
index 840f8ac8cb..d02fbf025b 100644
--- a/src/kernel/constraint.cpp
+++ b/src/kernel/constraint.cpp
@@ -12,28 +12,29 @@ struct constraint_cell {
     MK_LEAN_RC()
     constraint_kind m_kind;
     justification   m_jst;
-    constraint_cell(constraint_kind k, justification const & j):m_rc(1), m_kind(k), m_jst(j) {}
+    bool            m_relax_main_opaque;
+    constraint_cell(constraint_kind k, justification const & j, bool relax):m_rc(1), m_kind(k), m_jst(j), m_relax_main_opaque(relax) {}
 };
 struct eq_constraint_cell : public constraint_cell {
     expr m_lhs;
     expr m_rhs;
-    eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j):
-        constraint_cell(constraint_kind::Eq, j),
+    eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j, bool relax):
+        constraint_cell(constraint_kind::Eq, j, relax),
         m_lhs(lhs), m_rhs(rhs) {}
 };
 struct level_constraint_cell : public constraint_cell {
     level m_lhs;
     level m_rhs;
     level_constraint_cell(level const & lhs, level const & rhs, justification const & j):
-        constraint_cell(constraint_kind::LevelEq, j),
+        constraint_cell(constraint_kind::LevelEq, j, false),
         m_lhs(lhs), m_rhs(rhs) {}
 };
 struct choice_constraint_cell : public constraint_cell {
     expr      m_expr;
     choice_fn m_fn;
     unsigned  m_delay_factor;
-    choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j):
-        constraint_cell(constraint_kind::Choice, j),
+    choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax):
+        constraint_cell(constraint_kind::Choice, j, relax),
         m_expr(e), m_fn(fn), m_delay_factor(delay_factor) {}
 };
 
@@ -57,19 +58,20 @@ constraint & constraint::operator=(constraint && c) { LEAN_MOVE_REF(c); }
 constraint_kind constraint::kind() const { lean_assert(m_ptr); return m_ptr->m_kind; }
 justification const & constraint::get_justification() const { lean_assert(m_ptr); return m_ptr->m_jst; }
 
-constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
-    return constraint(new eq_constraint_cell(lhs, rhs, j));
+constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque) {
+    return constraint(new eq_constraint_cell(lhs, rhs, j, relax_main_opaque));
 }
 constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j) {
     return constraint(new level_constraint_cell(lhs, rhs, j));
 }
-constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j) {
+constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque) {
     lean_assert(is_meta(m));
-    return constraint(new choice_constraint_cell(m, fn, delay_factor, j));
+    return constraint(new choice_constraint_cell(m, fn, delay_factor, j, relax_main_opaque));
 }
 
 expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_lhs; }
 expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_rhs; }
+bool relax_main_opaque(constraint const & c) { return c.raw()->m_relax_main_opaque; }
 level const & cnstr_lhs_level(constraint const & c) {
     lean_assert(is_level_eq_cnstr(c));
     return static_cast<level_constraint_cell*>(c.raw())->m_lhs;
@@ -89,11 +91,11 @@ unsigned cnstr_delay_factor(constraint const & c) {
 constraint update_justification(constraint const & c, justification const & j) {
     switch (c.kind()) {
     case constraint_kind::Eq:
-        return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j);
+        return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j, relax_main_opaque(c));
     case constraint_kind::LevelEq:
         return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j);
     case constraint_kind::Choice:
-        return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j);
+        return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j, relax_main_opaque(c));
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h
index 7adc7ff12c..7cbfb67015 100644
--- a/src/kernel/constraint.h
+++ b/src/kernel/constraint.h
@@ -65,9 +65,10 @@ public:
     friend bool is_eqp(constraint const & c1, constraint const & c2) { return c1.m_ptr == c2.m_ptr; }
     friend void swap(constraint & l1, constraint & l2) { std::swap(l1, l2); }
 
-    friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+    friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
     friend constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
-    friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j);
+    friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j,
+                                      bool relax_main_opaque);
 
     constraint_cell * raw() const { return m_ptr; }
 };
@@ -75,9 +76,13 @@ public:
 inline bool operator==(constraint const & c1, constraint const & c2) { return c1.raw() == c2.raw(); }
 inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); }
 
-constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
+/**
+   \brief Create a unification constraint lhs =?= rhs
+   If \c relax_main_opaque is true, then opaque definitions from the main module are treated as transparent.
+*/
+constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
 constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
-constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j);
+constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque);
 
 inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
 inline bool is_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; }
@@ -89,6 +94,8 @@ constraint update_justification(constraint const & c, justification const & j);
 expr const & cnstr_lhs_expr(constraint const & c);
 /** \brief Return the rhs of an equality constraint. */
 expr const & cnstr_rhs_expr(constraint const & c);
+/** \brief Return true iff opaque definitions from the main module should be treated as transparent. */
+bool relax_main_opaque(constraint const & c);
 /** \brief Return the lhs of an level constraint. */
 level const & cnstr_lhs_level(constraint const & c);
 /** \brief Return the rhs of an level constraint. */
diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 0445597317..3fcf0f63a5 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -74,6 +74,7 @@ bool converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
 struct dummy_converter : public converter {
     virtual expr whnf(expr const & e, type_checker &) { return e; }
     virtual bool is_def_eq(expr const &, expr const &, type_checker &, delayed_justification &) { return true; }
+    virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
 };
 
 std::unique_ptr<converter> mk_dummy_converter() {
@@ -98,6 +99,10 @@ struct default_converter : public converter {
         m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) {
     }
 
+    constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+        return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
+    }
+
     optional<expr> expand_macro(expr const & m, type_checker & c) {
         lean_assert(is_macro(m));
         return macro_def(m).expand(m, get_extension(c));
@@ -552,6 +557,10 @@ struct default_converter : public converter {
     bool is_prop(expr const & e, type_checker & c) {
         return whnf(infer_type(c, e), c) == Prop;
     }
+
+    virtual optional<module_idx> get_module_idx() const {
+        return m_module_idx;
+    }
 };
 
 std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx,
diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index e2728d814a..1ebd8b42a0 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -20,6 +20,7 @@ public:
     virtual ~converter() {}
     virtual expr whnf(expr const & e, type_checker & c) = 0;
     virtual bool is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
+    virtual optional<module_idx> get_module_idx() const = 0;
     bool is_def_eq(expr const & t, expr const & s, type_checker & c);
 };
 
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index dcafd9bfce..44780c6f43 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -105,6 +105,10 @@ void type_checker::add_cnstr(constraint const & c) {
     m_cs.push_back(c);
 }
 
+constraint type_checker::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+    return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_conv->get_module_idx()));
+}
+
 optional<constraint> type_checker::next_cnstr() {
     if (m_cs_qhead < m_cs.size()) {
         constraint c = m_cs[m_cs_qhead];
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index a6c0e308fd..de1a2a0dea 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -105,6 +105,7 @@ class type_checker {
     expr infer_type(expr const & e);
     void copy_constraints(unsigned qhead, buffer<constraint> & new_cnstrs);
     extension_context & get_extension() { return m_tc_ctx; }
+    constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
 public:
     /**
        \brief Create a type checker for the given environment. The auxiliary names created by this
diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp
index f2796fec5f..f0411f06b6 100644
--- a/src/library/inductive_unifier_plugin.cpp
+++ b/src/library/inductive_unifier_plugin.cpp
@@ -45,7 +45,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     */
     lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl,
                                                 expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
-                                                buffer<constraint> & tc_cnstr_buffer) const {
+                                                buffer<constraint> & tc_cnstr_buffer, bool relax) const {
         lean_assert(is_constant(elim));
         environment const & env = tc.env();
         levels elim_lvls       = const_levels(elim);
@@ -78,12 +78,12 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
                 intro_type = tc.whnf(binding_body(intro_type), tc_cnstr_buffer);
                 lean_assert(!tc.next_cnstr());
             }
-            constraint c1      = mk_eq_cnstr(meta, hint, j);
+            constraint c1      = mk_eq_cnstr(meta, hint, j, relax);
             args[major_idx]    = hint;
             lean_assert(!tc.next_cnstr());
             expr reduce_elim   = tc.whnf(mk_app(elim, args), tc_cnstr_buffer);
             lean_assert(!tc.next_cnstr());
-            constraint c2      = mk_eq_cnstr(reduce_elim, t, j);
+            constraint c2      = mk_eq_cnstr(reduce_elim, t, j, relax);
             list<constraint> tc_cnstrs = to_list(tc_cnstr_buffer.begin(), tc_cnstr_buffer.end());
             alts.push_back(cons(c1, cons(c2, tc_cnstrs)));
         }
@@ -92,7 +92,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     }
 
     lazy_list<constraints> process_elim_meta_core(type_checker & tc, name_generator const & ngen,
-                                                  expr const & lhs, expr const & rhs, justification const & j) const {
+                                                  expr const & lhs, expr const & rhs, justification const & j, bool relax) const {
         lean_assert(inductive::is_elim_meta_app(tc, lhs));
         buffer<constraint> tc_cnstr_buffer;
         lean_assert(!tc.next_cnstr());
@@ -106,7 +106,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
         auto decls   = *inductive::is_inductive_decl(env, it_name);
         for (auto const & d : std::get<2>(decls)) {
             if (inductive::inductive_decl_name(d) == it_name)
-                return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, tc_cnstr_buffer);
+                return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, tc_cnstr_buffer, relax);
         }
         lean_unreachable(); // LCOV_EXCL_LINE
     }
@@ -122,10 +122,11 @@ public:
         expr const & lhs        = cnstr_lhs_expr(c);
         expr const & rhs        = cnstr_rhs_expr(c);
         justification const & j = c.get_justification();
+        bool relax = relax_main_opaque(c);
         if (inductive::is_elim_meta_app(tc, lhs))
-            return process_elim_meta_core(tc, ngen, lhs, rhs, j);
+            return process_elim_meta_core(tc, ngen, lhs, rhs, j, relax);
         else if (inductive::is_elim_meta_app(tc, rhs))
-            return process_elim_meta_core(tc, ngen, rhs, lhs, j);
+            return process_elim_meta_core(tc, ngen, rhs, lhs, j, relax);
         else
             return lazy_list<constraints>();
     }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 66e12f0f93..571a1a1dfb 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -1478,7 +1478,9 @@ static int constraint_tostring(lua_State * L) {
 }
 static int mk_eq_cnstr(lua_State * L) {
     int nargs = lua_gettop(L);
-    return push_constraint(L, mk_eq_cnstr(to_expr(L, 1), to_expr(L, 2), nargs == 3 ? to_justification(L, 3) : justification()));
+    return push_constraint(L, mk_eq_cnstr(to_expr(L, 1), to_expr(L, 2),
+                                          nargs >= 3 ? to_justification(L, 3) : justification(),
+                                          nargs >= 4 && lua_toboolean(L, 4)));
 }
 static int mk_level_eq_cnstr(lua_State * L) {
     int nargs = lua_gettop(L);
@@ -1508,7 +1510,7 @@ static choice_fn to_choice_fn(lua_State * L, int idx) {
                     if (is_constraint(L, -1))
                         r.push_back(constraints(to_constraint(L, -1)));
                     else if (is_expr(L, -1))
-                        r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification())));
+                        r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification(), false)));
                     else
                         r.push_back(to_list_constraint_ext(L, -1));
                     lua_pop(L, 1);
@@ -1526,13 +1528,15 @@ static int mk_choice_cnstr(lua_State * L) {
     expr m           = to_expr(L, 1);
     choice_fn fn     = to_choice_fn(L, 2);
     if (nargs == 2)
-        return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification()));
+        return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification(), false));
     else if (nargs == 3 && is_justification(L, 3))
-        return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3)));
+        return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3), false));
     else if (nargs == 3)
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification()));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification(), false));
+    else if (nargs == 4)
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), false));
     else
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4)));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), lua_toboolean(L, 5)));
 }
 
 static int constraint_expr(lua_State * L) {
diff --git a/src/library/opaque_hints.cpp b/src/library/opaque_hints.cpp
index efb6824a21..cf24341efe 100644
--- a/src/library/opaque_hints.cpp
+++ b/src/library/opaque_hints.cpp
@@ -45,15 +45,17 @@ environment expose_definition(environment const & env, name const & n) {
     ext.m_extra_opaque.erase(n);
     return update(env, ext);
 }
-environment set_main_module_opaque_defs(environment const & env, bool f) {
+environment set_hide_main_opaque(environment const & env, bool f) {
     auto ext = get_extension(env);
     ext.m_hide_module = f;
     return update(env, ext);
 }
-std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen) {
+bool get_hide_main_opaque(environment const & env) {
+    return get_extension(env).m_hide_module;
+}
+std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen, bool relax_main_opaque) {
     auto const & ext = get_extension(env);
-    return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module,
+    return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, !ext.m_hide_module && relax_main_opaque,
                                                                                           true, ext.m_extra_opaque)));
 }
 }
-
diff --git a/src/library/opaque_hints.h b/src/library/opaque_hints.h
index 1d77200684..b72002b97f 100644
--- a/src/library/opaque_hints.h
+++ b/src/library/opaque_hints.h
@@ -22,12 +22,11 @@ namespace lean {
 environment hide_definition(environment const & env, name const & n);
 /** \brief Undo the modification made with \c hide_definition. */
 environment expose_definition(environment const & env, name const & n);
-/**
-    \brief By default, the elaborator/unifier will treat the opaque
-    definitions of the current/main module as transparent. We can
-    change this behavior using this function.
+/** \brief By default, the elaborator/unifier will treat the opaque definitions of the current/main
+    module as transparent (when allowed). We can change this behavior using this function.
 */
-environment set_main_module_opaque_defs(environment const & env, bool f);
+environment set_hide_main_opaque(environment const & env, bool f);
+bool get_hide_main_opaque(environment const & env);
 /** \brief Create a type checker that takes the hints into account. */
-std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen);
+std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen, bool relax_main_opaque);
 }
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index ce299e4dc0..fd6e7317e6 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -92,7 +92,7 @@ static void remove_redundant_metas(buffer<expr> & metas) {
 }
 
 proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e,
-                                  bool add_meta, bool add_subgoals) {
+                                  bool add_meta, bool add_subgoals, bool relax_main_opaque) {
     goals const & gs = s.get_goals();
     if (empty(gs))
         return proof_state_seq();
@@ -119,7 +119,7 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios,
         }
     }
     list<expr> meta_lst = to_list(metas.begin(), metas.end());
-    lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), ios.get_options());
+    lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), relax_main_opaque, s.get_subst(), ios.get_options());
     return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
             name_generator new_ngen(ngen);
             type_checker tc(env, new_ngen.mk_child());
@@ -182,21 +182,21 @@ expr refresh_univ_metavars(expr const & e, name_generator & ngen) {
     }
 }
 
-tactic apply_tactic(expr const & e, bool refresh_univ_mvars) {
+tactic apply_tactic(expr const & e, bool relax_main_opaque, bool refresh_univ_mvars) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             if (refresh_univ_mvars) {
                 name_generator ngen    = s.get_ngen();
                 substitution new_subst = s.get_subst();
                 expr new_e = refresh_univ_metavars(new_subst.instantiate_all(e), ngen);
                 proof_state new_s(s.get_goals(), new_subst, ngen);
-                return apply_tactic_core(env, ios, new_s, new_e, true, true);
+                return apply_tactic_core(env, ios, new_s, new_e, true, true, relax_main_opaque);
             } else {
-                return apply_tactic_core(env, ios, s, e, true, true);
+                return apply_tactic_core(env, ios, s, e, true, true, relax_main_opaque);
             }
         });
 }
 
-tactic eassumption_tactic() {
+tactic eassumption_tactic(bool relax_main_opaque) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
             if (empty(gs))
@@ -206,7 +206,7 @@ tactic eassumption_tactic() {
             buffer<expr> hs;
             get_app_args(g.get_meta(), hs);
             for (expr const & h : hs) {
-                r = append(r, apply_tactic_core(env, ios, s, h, false, false));
+                r = append(r, apply_tactic_core(env, ios, s, h, false, false, relax_main_opaque));
             }
             return r;
         });
diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h
index be11161830..64015b8584 100644
--- a/src/library/tactic/apply_tactic.h
+++ b/src/library/tactic/apply_tactic.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "library/tactic/tactic.h"
 namespace lean {
-tactic apply_tactic(expr const & e, bool refresh_univ_mvars = true);
-tactic eassumption_tactic();
+tactic apply_tactic(expr const & e, bool relax_main_opaque = true, bool refresh_univ_mvars = true);
+tactic eassumption_tactic(bool relax_main_opaque = true);
 void open_apply_tactic(lua_State * L);
 }
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 7b857932dd..50f3e465c2 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -209,7 +209,7 @@ unify_status unify_simple(substitution & s, constraint const & c) {
         return unify_status::Unsupported;
 }
 
-static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification());
+static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification(), false);
 static unsigned g_group_size = 1u << 29;
 static unsigned g_cnstr_group_first_index[6] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size};
 static unsigned get_group_first_index(cnstr_group g) {
@@ -241,7 +241,7 @@ struct unifier_fn {
     name_generator   m_ngen;
     substitution     m_subst;
     unifier_plugin   m_plugin;
-    type_checker_ptr m_tc;
+    type_checker_ptr m_tc[2];
     bool             m_use_exception; //!< True if we should throw an exception when there are no more solutions.
     unsigned         m_max_steps;
     unsigned         m_num_steps;
@@ -292,14 +292,17 @@ struct unifier_fn {
             m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst), m_cnstrs(u.m_cnstrs),
             m_mvar_occs(u.m_mvar_occs) {
             u.m_next_assumption_idx++;
-            u.m_tc->push();
+            u.m_tc[0]->push();
+            u.m_tc[1]->push();
         }
 
         /** \brief Restore unifier's state with saved values, and update m_assumption_idx and m_failed_justifications. */
         void restore_state(unifier_fn & u) {
             lean_assert(u.in_conflict());
-            u.m_tc->pop();   // restore type checker state
-            u.m_tc->push();
+            u.m_tc[0]->pop();   // restore type checker state
+            u.m_tc[1]->pop();   // restore type checker state
+            u.m_tc[0]->push();
+            u.m_tc[1]->push();
             u.m_subst     = m_subst;
             u.m_cnstrs    = m_cnstrs;
             u.m_mvar_occs = m_mvar_occs;
@@ -333,8 +336,9 @@ struct unifier_fn {
                name_generator const & ngen, substitution const & s,
                bool use_exception, unsigned max_steps):
         m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)),
-        m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())),
         m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) {
+        m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false);
+        m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true);
         m_next_assumption_idx = 0;
         m_next_cidx = 0;
         m_first     = true;
@@ -403,9 +407,12 @@ struct unifier_fn {
         return cidx;
     }
 
-    /** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j */
-    bool is_def_eq(expr const & t1, expr const & t2, justification const & j) {
-        if (m_tc->is_def_eq(t1, t2, j)) {
+    /** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j
+
+        \remark If relax is true then opaque definitions from the main module are treated as transparent.
+    */
+    bool is_def_eq(expr const & t1, expr const & t2, justification const & j, bool relax) {
+        if (m_tc[relax]->is_def_eq(t1, t2, j)) {
             return true;
         } else {
             set_conflict(j);
@@ -417,21 +424,23 @@ struct unifier_fn {
        \brief Assign \c v to metavariable \c m with justification \c j.
        The type of v and m are inferred, and is_def_eq is invoked.
        Any constraint that contains \c m is revisited.
+
+       \remark If relax is true then opaque definitions from the main module are treated as transparent.
     */
-    bool assign(expr const & m, expr const & v, justification const & j) {
+    bool assign(expr const & m, expr const & v, justification const & j, bool relax) {
         lean_assert(is_metavar(m));
         m_subst.assign(m, v, j);
         expr m_type = mlocal_type(m);
         expr v_type;
         try {
-            v_type = m_tc->infer(v);
+            v_type = m_tc[relax]->infer(v);
         } catch (kernel_exception & e) {
             set_conflict(j);
             return false;
         }
         if (in_conflict())
             return false;
-        if (!is_def_eq(m_type, v_type, j))
+        if (!is_def_eq(m_type, v_type, j, relax))
             return false;
         auto it = m_mvar_occs.find(mlocal_name(m));
         if (it) {
@@ -463,7 +472,7 @@ struct unifier_fn {
        The method returns \c Failed if \c rhs contains <tt>?m</tt>, or it contains a local constant not in <tt>{l_1, ..., l_n}</tt>.
        Otherwise, it returns \c Continue.
     */
-    status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j) {
+    status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
         if (!is_meta(lhs))
             return Continue;
         buffer<expr> locals;
@@ -478,7 +487,7 @@ struct unifier_fn {
             return Continue;
         case l_true:
             lean_assert(!m_subst.is_assigned(*m));
-            if (assign(*m, lambda_abstract_locals(rhs, locals), j)) {
+            if (assign(*m, lambda_abstract_locals(rhs, locals), j, relax)) {
                 return Solved;
             } else {
                 return Failed;
@@ -509,7 +518,8 @@ struct unifier_fn {
             expr rhs = rhs_jst.first;
             if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) {
                 return mk_pair(mk_eq_cnstr(lhs, rhs,
-                                           mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second)),
+                                           mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second),
+                                           relax_main_opaque(c)),
                                true);
             }
         } else if (is_level_eq_cnstr(c)) {
@@ -530,19 +540,20 @@ struct unifier_fn {
         expr const & lhs = cnstr_lhs_expr(c);
         expr const & rhs = cnstr_rhs_expr(c);
         justification const & jst = c.get_justification();
+        bool relax = relax_main_opaque(c);
 
         if (lhs == rhs)
             return Solved; // trivial constraint
 
         // Update justification using the justification of the instantiated metavariables
         if (!has_metavar(lhs) && !has_metavar(rhs)) {
-            return is_def_eq(lhs, rhs, jst) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, jst, relax) ? Solved : Failed;
         }
 
         // Handle higher-order pattern matching.
-        status st = process_metavar_eq(lhs, rhs, jst);
+        status st = process_metavar_eq(lhs, rhs, jst, relax);
         if (st != Continue) return st;
-        st = process_metavar_eq(rhs, lhs, jst);
+        st = process_metavar_eq(rhs, lhs, jst, relax);
         if (st != Continue) return st;
 
         return Continue;
@@ -589,11 +600,11 @@ struct unifier_fn {
         expr lhs = instantiate_meta(cnstr_lhs_expr(c), j);
         expr rhs = instantiate_meta(cnstr_rhs_expr(c), j);
         if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
-            return is_def_eq(lhs, rhs, j) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
         lhs = instantiate_meta_args(lhs, j);
         rhs = instantiate_meta_args(rhs, j);
         if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
-            return is_def_eq(lhs, rhs, j) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
         return Continue;
     }
 
@@ -608,6 +619,7 @@ struct unifier_fn {
 
         expr const & lhs = cnstr_lhs_expr(c);
         expr const & rhs = cnstr_rhs_expr(c);
+        bool relax = relax_main_opaque(c);
 
         if (is_eq_deltas(lhs, rhs)) {
             // we need to create a backtracking point for this one
@@ -617,7 +629,7 @@ struct unifier_fn {
             unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
             add_meta_occ(lhs, cidx);
             add_meta_occ(rhs, cidx);
-        } else if (m_plugin->delay_constraint(*m_tc, c)) {
+        } else if (m_plugin->delay_constraint(*m_tc[relax], c)) {
             unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
             add_meta_occs(lhs, cidx);
             add_meta_occs(rhs, cidx);
@@ -749,7 +761,8 @@ struct unifier_fn {
     }
 
     void pop_case_split() {
-        m_tc->pop();
+        m_tc[0]->pop();
+        m_tc[1]->pop();
         m_case_splits.pop_back();
     }
 
@@ -835,26 +848,28 @@ struct unifier_fn {
             return lazy_list<constraints>();
         justification const & j = c.get_justification();
         buffer<constraint> cs;
-        lean_assert(!m_tc->next_cnstr());
-        if (!m_tc->is_def_eq(f_lhs, f_rhs, j, cs))
+        bool relax = relax_main_opaque(c);
+        lean_assert(!m_tc[relax]->next_cnstr());
+        if (!m_tc[relax]->is_def_eq(f_lhs, f_rhs, j, cs))
             return lazy_list<constraints>();
         buffer<expr> args_lhs, args_rhs;
         get_app_args(lhs, args_lhs);
         get_app_args(rhs, args_rhs);
         if (args_lhs.size() != args_rhs.size())
             return lazy_list<constraints>();
-        lean_assert(!m_tc->next_cnstr());
+        lean_assert(!m_tc[relax]->next_cnstr());
         for (unsigned i = 0; i < args_lhs.size(); i++)
-            if (!m_tc->is_def_eq(args_lhs[i], args_rhs[i], j, cs))
+            if (!m_tc[relax]->is_def_eq(args_lhs[i], args_rhs[i], j, cs))
                 return lazy_list<constraints>();
         return lazy_list<constraints>(to_list(cs.begin(), cs.end()));
     }
 
     bool process_plugin_constraint(constraint const & c) {
+        bool relax = relax_main_opaque(c);
         lean_assert(!is_choice_cnstr(c));
-        lean_assert(!m_tc->next_cnstr());
-        lazy_list<constraints> alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child());
-        lean_assert(!m_tc->next_cnstr());
+        lean_assert(!m_tc[relax]->next_cnstr());
+        lazy_list<constraints> alts = m_plugin->solve(*m_tc[relax], c, m_ngen.mk_child());
+        lean_assert(!m_tc[relax]->next_cnstr());
         alts = append(alts, process_const_const_cnstr(c));
         return process_lazy_constraints(alts, c.get_justification());
     }
@@ -864,8 +879,9 @@ struct unifier_fn {
         expr const &   m            = cnstr_expr(c);
         choice_fn const & fn        = cnstr_choice_fn(c);
         expr m_type;
+        bool relax = relax_main_opaque(c);
         try {
-            m_type                  = m_tc->infer(m);
+            m_type                  = m_tc[relax]->infer(m);
         } catch (kernel_exception &) {
             set_conflict(c.get_justification());
             return false;
@@ -920,8 +936,9 @@ struct unifier_fn {
         expr rhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), const_levels(rhs_fn));
         expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data());
         expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data());
+        bool relax = relax_main_opaque(c);
         buffer<constraint> cs2;
-        if (m_tc->is_def_eq(t, s, j, cs2)) {
+        if (m_tc[relax]->is_def_eq(t, s, j, cs2)) {
             // create a case split
             a = mk_assumption_justification(m_next_assumption_idx);
             add_case_split(std::unique_ptr<case_split>(new simple_case_split(*this, j, to_list(cs2.begin(), cs2.end()))));
@@ -941,7 +958,7 @@ struct unifier_fn {
         unsigned i = lhs_args.size();
         while (i > 0) {
             --i;
-            if (!is_def_eq(lhs_args[i], rhs_args[i], new_j))
+            if (!is_def_eq(lhs_args[i], rhs_args[i], new_j, relax))
                 return false;
         }
         return true;
@@ -979,19 +996,19 @@ struct unifier_fn {
     }
 
     /** \see ensure_sufficient_args */
-    optional<expr> ensure_sufficient_args_core(expr mtype, unsigned i, buffer<expr> const & margs) {
+    optional<expr> ensure_sufficient_args_core(expr mtype, unsigned i, buffer<expr> const & margs, bool relax) {
         if (i == margs.size())
             return some_expr(mtype);
-        mtype = m_tc->ensure_pi(mtype);
+        mtype = m_tc[relax]->ensure_pi(mtype);
         try {
-            if (!m_tc->is_def_eq(binding_domain(mtype), m_tc->infer(margs[i])))
+            if (!m_tc[relax]->is_def_eq(binding_domain(mtype), m_tc[relax]->infer(margs[i])))
                 return none_expr();
         } catch (kernel_exception &) {
             return none_expr();
         }
         expr local = mk_local_for(mtype);
         expr body  = instantiate(binding_body(mtype), local);
-        auto new_body = ensure_sufficient_args_core(body, i+1, margs);
+        auto new_body = ensure_sufficient_args_core(body, i+1, margs, relax);
         if (!new_body)
             return none_expr();
         return some_expr(Pi(local, *new_body));
@@ -1001,7 +1018,8 @@ struct unifier_fn {
        \brief Make sure mtype is a Pi of size at least margs.size().
        If it is not, we use ensure_pi and (potentially) add new constaints to enforce it.
     */
-    optional<expr> ensure_sufficient_args(expr const & mtype, buffer<expr> const & margs, buffer<constraint> & cs, justification const & j) {
+    optional<expr> ensure_sufficient_args(expr const & mtype, buffer<expr> const & margs, buffer<constraint> & cs, justification const & j,
+                                          bool relax) {
         expr t = mtype;
         unsigned num = 0;
         while (is_pi(t)) {
@@ -1010,13 +1028,13 @@ struct unifier_fn {
         }
         if (num == margs.size())
             return some_expr(mtype);;
-        lean_assert(!m_tc->next_cnstr()); // make sure there are no pending constraints
+        lean_assert(!m_tc[relax]->next_cnstr()); // make sure there are no pending constraints
         // We must create a scope to make sure no constraints "leak" into the current state.
-        type_checker::scope scope(*m_tc);
-        auto new_mtype = ensure_sufficient_args_core(mtype, 0, margs);
+        type_checker::scope scope(*m_tc[relax]);
+        auto new_mtype = ensure_sufficient_args_core(mtype, 0, margs, relax);
         if (!new_mtype)
             return none_expr();
-        while (auto c = m_tc->next_cnstr())
+        while (auto c = m_tc[relax]->next_cnstr())
             cs.push_back(update_justification(*c, mk_composite1(c->get_justification(), j)));
         return new_mtype;
     }
@@ -1073,13 +1091,13 @@ struct unifier_fn {
                   - variable (if g is a local constant equal to a_i)
     */
     void mk_flex_rigid_app_cnstrs(expr const & m, buffer<expr> const & margs, expr const & f, expr const & rhs, justification const & j,
-                                  buffer<constraints> & alts) {
+                                  buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(is_app(rhs));
         lean_assert(is_constant(f) || is_var(f));
         buffer<constraint> cs;
         expr mtype = mlocal_type(m);
-        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
+        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
         if (!new_mtype) return;
         mtype = *new_mtype;
         buffer<expr> rargs;
@@ -1090,13 +1108,13 @@ struct unifier_fn {
                 sargs.push_back(*v);
             } else {
                 expr maux = mk_aux_metavar_for(m_ngen, mtype);
-                cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j));
+                cs.push_back(mk_eq_cnstr(mk_app(maux, margs), rarg, j, relax));
                 sargs.push_back(mk_app_vars(maux, margs.size()));
             }
         }
         expr v = mk_app(f, sargs);
         v = mk_lambda_for(mtype, v);
-        cs.push_back(mk_eq_cnstr(m, v, j));
+        cs.push_back(mk_eq_cnstr(m, v, j, relax));
         alts.push_back(to_list(cs.begin(), cs.end()));
     }
 
@@ -1112,25 +1130,25 @@ struct unifier_fn {
        where l is a fresh local constant.
     */
     void mk_bindings_imitation(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
-                               buffer<constraints> & alts) {
+                               buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(is_binding(rhs));
         buffer<constraint> cs;
         expr mtype = mlocal_type(m);
-        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
+        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
         if (!new_mtype) return;
         mtype = *new_mtype;
         expr maux1  = mk_aux_metavar_for(m_ngen, mtype);
-        cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j));
+        cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j, relax));
         expr dontcare;
         expr tmp_pi = mk_pi(binding_name(rhs), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context
         expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context
         expr maux2  = mk_aux_metavar_for(m_ngen, mtype2);
         expr new_local = mk_local_for(rhs);
-        cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j));
+        cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j, relax));
         expr v = update_binding(rhs, mk_app_vars(maux1, margs.size()), mk_app_vars(maux2, margs.size() + 1));
         v = mk_lambda_for(mtype, v);
-        cs.push_back(mk_eq_cnstr(m, v, j));
+        cs.push_back(mk_eq_cnstr(m, v, j, relax));
         alts.push_back(to_list(cs.begin(), cs.end()));
     }
 
@@ -1141,12 +1159,12 @@ struct unifier_fn {
         Then solve (?m a_1 ... a_k) =?= rhs, by returning the constraint
                  ?m  =?= fun (x1 ... x_k), rhs
     */
-    void mk_simple_imitation(expr const & m, expr const & rhs, justification const & j, buffer<constraints> & alts) {
+    void mk_simple_imitation(expr const & m, expr const & rhs, justification const & j, buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(is_sort(rhs) || is_constant(rhs));
         expr const & mtype = mlocal_type(m);
         buffer<constraint> cs;
-        cs.push_back(mk_eq_cnstr(m, mk_lambda_for(mtype, rhs), j));
+        cs.push_back(mk_eq_cnstr(m, mk_lambda_for(mtype, rhs), j, relax));
         alts.push_back(to_list(cs.begin(), cs.end()));
     }
 
@@ -1162,24 +1180,24 @@ struct unifier_fn {
                ?m  =?= fun (x_1 ... x_k), M((?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k))
     */
     void mk_macro_imitation(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
-                            buffer<constraints> & alts) {
+                            buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(is_macro(rhs));
         buffer<constraint> cs;
         expr mtype = mlocal_type(m);
-        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j);
+        auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
         if (!new_mtype) return;
         mtype = *new_mtype;
         // create an auxiliary metavariable for each macro argument
         buffer<expr> sargs;
         for (unsigned i = 0; i < macro_num_args(rhs); i++) {
             expr maux = mk_aux_metavar_for(m_ngen, mtype);
-            cs.push_back(mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j));
+            cs.push_back(mk_eq_cnstr(mk_app(maux, margs), macro_arg(rhs, i), j, relax));
             sargs.push_back(mk_app_vars(maux, margs.size()));
         }
         expr v = mk_macro(macro_def(rhs), sargs.size(), sargs.data());
         v = mk_lambda_for(mtype, v);
-        cs.push_back(mk_eq_cnstr(m, v, j));
+        cs.push_back(mk_eq_cnstr(m, v, j, relax));
         alts.push_back(to_list(cs.begin(), cs.end()));
     }
 
@@ -1198,17 +1216,17 @@ struct unifier_fn {
        to alts as a possible solution.
     */
     void mk_simple_nonlocal_projection(expr const & m, buffer<expr> const & margs, unsigned i, expr const & rhs, justification const & j,
-                              buffer<constraints> & alts) {
+                                       buffer<constraints> & alts, bool relax) {
         expr const & mtype = mlocal_type(m);
         unsigned vidx = margs.size() - i - 1;
         expr const & marg = margs[i];
         buffer<constraint> cs;
-        if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) {
+        if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
             // Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them.
             // The unifier assumes the eq constraints are reduced.
-            if (m_tc->is_def_eq(marg, rhs, j, cs)) {
+            if (m_tc[relax]->is_def_eq(marg, rhs, j, cs)) {
                 expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
-                cs.push_back(mk_eq_cnstr(m, v, j));
+                cs.push_back(mk_eq_cnstr(m, v, j, relax));
                 alts.push_back(to_list(cs.begin(), cs.end()));
             }
         }
@@ -1232,7 +1250,7 @@ struct unifier_fn {
 
     */
     void mk_simple_projections(expr const & m, buffer<expr> const & margs, expr const & rhs, justification const & j,
-                                buffer<constraints> & alts) {
+                               buffer<constraints> & alts, bool relax) {
         lean_assert(is_metavar(m));
         lean_assert(!is_meta(rhs));
         expr const & mtype = mlocal_type(m);
@@ -1243,13 +1261,13 @@ struct unifier_fn {
             expr const & marg = margs[i];
             if ((!is_local(marg) && !is_local(rhs)) || (is_meta(marg) && is_local(rhs))) {
                 // if rhs is not local, then we only add projections for the nonlocal arguments of lhs
-                mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts);
+                mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts, relax);
             } else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) {
                 // if the argument is local, and rhs is equal to it, then we also add a projection
                 buffer<constraint> cs;
-                if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j)) {
+                if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
                     expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
-                    cs.push_back(mk_eq_cnstr(m, v, j));
+                    cs.push_back(mk_eq_cnstr(m, v, j, relax));
                     alts.push_back(to_list(cs.begin(), cs.end()));
                 }
             }
@@ -1257,7 +1275,7 @@ struct unifier_fn {
     }
 
     /** \brief Process a flex rigid constraint */
-    bool process_flex_rigid(expr const & lhs, expr const & rhs, justification const & j) {
+    bool process_flex_rigid(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
         lean_assert(is_meta(lhs));
         lean_assert(!is_meta(rhs));
         buffer<expr> margs;
@@ -1266,7 +1284,7 @@ struct unifier_fn {
             // Make sure that if marg is reducible to a local constant, then it is replaced with it.
             // We need that because of the optimization based on is_easy_flex_rigid_arg
             if (!is_local(marg)) {
-                expr new_marg = m_tc->whnf(marg);
+                expr new_marg = m_tc[relax]->whnf(marg);
                 if (is_local(new_marg))
                     marg = new_marg;
             }
@@ -1276,19 +1294,19 @@ struct unifier_fn {
         case expr_kind::Var: case expr_kind::Meta:
             lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::Local:
-            mk_simple_projections(m, margs, rhs, j, alts);
+            mk_simple_projections(m, margs, rhs, j, alts, relax);
             break;
         case expr_kind::Sort: case expr_kind::Constant:
-            mk_simple_projections(m, margs, rhs, j, alts);
-            mk_simple_imitation(m, rhs, j, alts);
+            mk_simple_projections(m, margs, rhs, j, alts, relax);
+            mk_simple_imitation(m, rhs, j, alts, relax);
             break;
         case expr_kind::Pi: case expr_kind::Lambda:
-            mk_simple_projections(m, margs, rhs, j, alts);
-            mk_bindings_imitation(m, margs, rhs, j, alts);
+            mk_simple_projections(m, margs, rhs, j, alts, relax);
+            mk_bindings_imitation(m, margs, rhs, j, alts, relax);
             break;
         case expr_kind::Macro:
-            mk_simple_projections(m, margs, rhs, j, alts);
-            mk_macro_imitation(m, margs, rhs, j, alts);
+            mk_simple_projections(m, margs, rhs, j, alts, relax);
+            mk_macro_imitation(m, margs, rhs, j, alts, relax);
             break;
         case expr_kind::App: {
             expr const & f = get_app_fn(rhs);
@@ -1299,17 +1317,17 @@ struct unifier_fn {
                     --i;
                     expr const & marg = margs[i];
                     if (is_local(marg) && mlocal_name(marg) == mlocal_name(f))
-                        mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j, alts);
+                        mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j, alts, relax);
                     else
-                        mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts);
+                        mk_simple_nonlocal_projection(m, margs, i, rhs, j, alts, relax);
                 }
             } else if (is_constant(f)) {
-                mk_simple_projections(m, margs, rhs, j, alts);
-                mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j, alts);
+                mk_simple_projections(m, margs, rhs, j, alts, relax);
+                mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j, alts, relax);
             } else {
-                expr new_rhs = m_tc->whnf(rhs);
+                expr new_rhs = m_tc[relax]->whnf(rhs);
                 lean_assert(new_rhs != rhs);
-                return is_def_eq(lhs, new_rhs, j);
+                return is_def_eq(lhs, new_rhs, j, relax);
             }
             break;
         }}
@@ -1330,12 +1348,13 @@ struct unifier_fn {
     /** \brief Process a flex rigid constraint */
     bool process_flex_rigid(constraint const & c) {
         lean_assert(is_flex_rigid(c));
-        expr lhs = cnstr_lhs_expr(c);
-        expr rhs = cnstr_rhs_expr(c);
+        expr lhs   = cnstr_lhs_expr(c);
+        expr rhs   = cnstr_rhs_expr(c);
+        bool relax = relax_main_opaque(c);
         if (is_meta(lhs))
-            return process_flex_rigid(lhs, rhs, c.get_justification());
+            return process_flex_rigid(lhs, rhs, c.get_justification(), relax);
         else
-            return process_flex_rigid(rhs, lhs, c.get_justification());
+            return process_flex_rigid(rhs, lhs, c.get_justification(), relax);
     }
 
     bool process_flex_flex(constraint const & c) {
@@ -1358,18 +1377,20 @@ struct unifier_fn {
             if (mlocal_name(lhs_args[i]) != mlocal_name(rhs_args[i]))
                 break;
         if (i == lhs_args.size())
-            return assign(ml, mr, c.get_justification());
+            return assign(ml, mr, c.get_justification(), relax_main_opaque(c));
         return true;
     }
 
     void consume_tc_cnstrs() {
-        while (true) {
-            if (in_conflict())
-                return;
-            if (auto c = m_tc->next_cnstr()) {
-                process_constraint(*c);
-            } else {
-                break;
+        for (unsigned i = 0; i < 2; i++) {
+            while (true) {
+                if (in_conflict())
+                    return;
+                if (auto c = m_tc[i]->next_cnstr()) {
+                    process_constraint(*c);
+                } else {
+                    break;
+                }
             }
         }
     }
@@ -1417,7 +1438,8 @@ struct unifier_fn {
         } else {
             auto r = instantiate_metavars(c);
             c = r.first;
-            lean_assert(!m_tc->next_cnstr());
+            lean_assert(!m_tc[0]->next_cnstr());
+            lean_assert(!m_tc[1]->next_cnstr());
             bool modified = r.second;
             if (is_level_eq_cnstr(c)) {
                 if (modified)
@@ -1432,7 +1454,7 @@ struct unifier_fn {
                 if (is_delta_cnstr(c)) {
                     return process_delta(c);
                 } else if (modified) {
-                    return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification());
+                    return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification(), relax_main_opaque(c));
                 } else if (is_flex_rigid(c)) {
                     return process_flex_rigid(c);
                 } else if (is_flex_flex(c)) {
@@ -1510,21 +1532,21 @@ lazy_list<substitution> unify(environment const & env,  unsigned num_cs, constra
     return unify(env, num_cs, cs, ngen, use_exception, get_unifier_max_steps(o));
 }
 
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
-                              unsigned max_steps) {
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+                              bool relax, substitution const & s, unsigned max_steps) {
     substitution new_s = s;
     expr _lhs = new_s.instantiate(lhs);
     expr _rhs = new_s.instantiate(rhs);
     auto u = std::make_shared<unifier_fn>(env, 0, nullptr, ngen, new_s, false, max_steps);
-    if (!u->m_tc->is_def_eq(_lhs, _rhs))
+    if (!u->m_tc[relax]->is_def_eq(_lhs, _rhs))
         return lazy_list<substitution>();
     else
         return unify(u);
 }
 
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
-                              substitution const & s, options const & o) {
-    return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o));
+                              bool relax, substitution const & s, options const & o) {
+    return unify(env, lhs, rhs, ngen, relax, s, get_unifier_max_steps(o));
 }
 
 static int unify_simple(lua_State * L) {
@@ -1646,10 +1668,12 @@ static int unify(lua_State * L) {
     lazy_list<substitution> r;
     environment const & env = to_environment(L, 1);
     if (is_expr(L, 2)) {
-        if (nargs == 6)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_options(L, 6));
+        if (nargs == 7)
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6), to_options(L, 7));
+        else if (nargs == 6)
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6), options());
         else
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), options());
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5));
     } else {
         buffer<constraint> cs;
         to_constraint_buffer(L, 2, cs);
diff --git a/src/library/unifier.h b/src/library/unifier.h
index 26e09f3e9b..c64b4169ce 100644
--- a/src/library/unifier.h
+++ b/src/library/unifier.h
@@ -40,10 +40,10 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constrai
                               bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
 lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
                               bool use_exception, options const & o);
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, bool relax_main_opaque,
                               substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
-                              options const & o);
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+                              bool relax_main_opaque, substitution const & s, options const & o);
 
 /**
     The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed
diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp
index 0495475b50..0b46fb6a2c 100644
--- a/src/tests/library/unifier.cpp
+++ b/src/tests/library/unifier.cpp
@@ -18,7 +18,7 @@ static void tst1() {
     expr m  = mk_metavar("m", A);
     expr t1 = f(m, m);
     expr t2 = f(a, b);
-    auto r = unify(env, t1, t2, ngen);
+    auto r = unify(env, t1, t2, ngen, false);
     lean_assert(!r.pull());
 }
 
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index d099faeaf4..a08ef8b4a7 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -69,6 +69,7 @@ variable div : Π (x y : nat) {H : not_zero y}, nat
 
 variables a b : nat
 
+set_option pp.implicit true
 opaque_hint (hiding [module])
 check div a (succ b)
 check (λ H : not_zero b, div a b)
diff --git a/tests/lean/run/uni.lean b/tests/lean/run/uni.lean
index f4fa23eaeb..5f6d9af1a9 100644
--- a/tests/lean/run/uni.lean
+++ b/tests/lean/run/uni.lean
@@ -27,7 +27,7 @@ print(env:whnf(t(m)))
 
 function test_unify(env, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
+   local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: ")
diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean
index 407b1a0110..a557e76106 100644
--- a/tests/lean/run/uni2.lean
+++ b/tests/lean/run/uni2.lean
@@ -30,7 +30,7 @@ print(env:whnf(t(m)))
 
 function test_unify(env, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
+   local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: ")
diff --git a/tests/lean/run/univ2.lean b/tests/lean/run/univ2.lean
new file mode 100644
index 0000000000..786d1a8c98
--- /dev/null
+++ b/tests/lean/run/univ2.lean
@@ -0,0 +1,11 @@
+import standard
+
+hypothesis I : Type
+definition F (X : Type) : Type := (X → Prop) → Prop
+hypothesis unfold : I → F I
+hypothesis fold   : F I → I
+hypothesis iso1 : ∀x, fold (unfold x) = x
+
+variable sorry {A : Type} : A
+theorem iso2 : ∀x, fold (unfold x) = x
+:= sorry
diff --git a/tests/lua/unify2.lua b/tests/lua/unify2.lua
index f1cf56e9b2..a04282beaa 100644
--- a/tests/lua/unify2.lua
+++ b/tests/lua/unify2.lua
@@ -1,6 +1,6 @@
 function test_unify(env, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
+   local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: ")
diff --git a/tests/lua/unify4.lua b/tests/lua/unify4.lua
index a94af1e47f..f01b933f6d 100644
--- a/tests/lua/unify4.lua
+++ b/tests/lua/unify4.lua
@@ -1,6 +1,6 @@
 function test_unify(env, m, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
+   local ss = unify(env, lhs, rhs, name_generator(), true, substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: " .. tostring(s:instantiate(m)))