diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index ba2809383..d6770f985 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -512,7 +512,13 @@ expr  type_check(expr const & e, ro_environment const & env, context const & ctx
 bool is_convertible(expr const & given, expr const & expected, ro_environment const & env, context const & ctx) {
     return type_checker(env).is_convertible(given, expected, ctx);
 }
+bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv) {
+    return type_checker(env).is_proposition(e, ctx, menv);
+}
+bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, metavar_env const & menv) {
+    return is_proposition(e, env, ctx, some_menv(menv));
+}
 bool is_proposition(expr const & e, ro_environment const & env, context const & ctx) {
-    return type_checker(env).is_proposition(e, ctx);
+    return is_proposition(e, env, ctx, none_menv());
 }
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 697defcab..3cb3e4350 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -111,5 +111,7 @@ public:
 };
 expr type_check(expr const & e, ro_environment const & env, context const & ctx = context());
 bool is_convertible(expr const & t1, expr const & t2, ro_environment const & env, context const & ctx = context());
+bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv);
+bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, metavar_env const & menv);
 bool is_proposition(expr const & e, ro_environment const & env, context const & ctx = context());
 }
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index c76ae686d..db14c618f 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -80,8 +80,8 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
                             update_hypotheses_fn add_hypothesis(hs);
                             hypotheses extra_hs;
                             while (is_pi(arg_type)) {
-                                expr d   = abst_domain(arg_type);
-                                name n   = arg_to_hypothesis_name(env, context(), abst_name(arg_type), d);
+                                expr d = abst_domain(arg_type);
+                                name n = arg_to_hypothesis_name(abst_name(arg_type), d, env, context(), new_menv);
                                 n   = add_hypothesis(n, d);
                                 extra_hs.emplace_front(n, d);
                                 arg_type = instantiate(abst_body(arg_type), mk_constant(n, d), new_menv);
diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index ab158985a..12ffdc33b 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/src/library/tactic/proof_state.cpp
@@ -88,8 +88,8 @@ void proof_state::get_goal_names(name_set & r) const {
     }
 }
 
-name arg_to_hypothesis_name(ro_environment const & env, context const & ctx, name const & n, expr const & d) {
-    if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx))
+name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv) {
+    if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx, menv))
         return name("H");
     else
         return n;
@@ -100,7 +100,7 @@ static name g_main("main");
 proof_state to_proof_state(ro_environment const & env, context ctx, expr t) {
     list<std::pair<name, expr>> extra_binders;
     while (is_pi(t)) {
-        name vname = arg_to_hypothesis_name(env, ctx, abst_name(t), abst_domain(t));
+        name vname = arg_to_hypothesis_name(abst_name(t), abst_domain(t), env, ctx);
         extra_binders.emplace_front(vname, abst_domain(t));
         ctx = extend(ctx, vname, abst_domain(t));
         t   = abst_body(t);
diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h
index a5dee697c..5cb903ecf 100644
--- a/src/library/tactic/proof_state.h
+++ b/src/library/tactic/proof_state.h
@@ -124,7 +124,11 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state & s)
     \brief Return a name based on \c n that is suitable to be used as a hypothesis name
     It basically renames \c n to 'H' if \c d is a proposition and \c n is the default arrow binder name.
 */
-name arg_to_hypothesis_name(ro_environment const & env, context const & ctx, name const & n, expr const & d);
+name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx,
+                            optional<metavar_env> const & menv = none_menv());
+inline name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, metavar_env const & menv) {
+    return arg_to_hypothesis_name(n, d, env, ctx, some_menv(menv));
+}
 
 UDATA_DEFS_CORE(goals)
 UDATA_DEFS(proof_state)