diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index ed10f69b2..795e9b415 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1806,22 +1806,24 @@ class parser::imp {
             if (has_metavar(mvar_type))
                 throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type,
                                                         "failed to synthesize metavar, its type contains metavariables");
-            if (!is_proposition(mvar_type, m_env, mvar_ctx))
-                throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type, "failed to synthesize metavar, its type is not a proposition");
-            proof_state s = to_proof_state(m_env, mvar_ctx, mvar_type);
-            std::pair<optional<tactic>, pos_info> hint_and_pos = get_tactic_for(mvar);
-            if (hint_and_pos.first) {
-                // metavariable has an associated tactic hint
-                s = apply_tactic(s, *(hint_and_pos.first), hint_and_pos.second).first;
-                menv->assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type));
-            } else {
-                if (curr_is_period()) {
-                    display_proof_state_if_interactive(s);
-                    show_tactic_prompt();
-                    next();
+            try {
+                proof_state s = to_proof_state(m_env, mvar_ctx, mvar_type);
+                std::pair<optional<tactic>, pos_info> hint_and_pos = get_tactic_for(mvar);
+                if (hint_and_pos.first) {
+                    // metavariable has an associated tactic hint
+                    s = apply_tactic(s, *(hint_and_pos.first), hint_and_pos.second).first;
+                    menv->assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type));
+                } else {
+                    if (curr_is_period()) {
+                        display_proof_state_if_interactive(s);
+                        show_tactic_prompt();
+                        next();
+                    }
+                    expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type);
+                    menv->assign(mvar, mvar_val);
                 }
-                expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type);
-                menv->assign(mvar, mvar_val);
+            } catch (type_is_not_proposition_exception &) {
+                throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type, "failed to synthesize metavar, its type is not a proposition");
             }
         }
         return menv->instantiate_metavars(val);
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index ec7af9a9a..f55a60346 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -426,6 +426,7 @@ inline expr mk_eq(expr const & l, expr const & r) { return expr(new expr_eq(l, r
 inline expr Eq(expr const & l, expr const & r) { return mk_eq(l, r); }
 inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
 inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
+inline bool is_default_arrow_var_name(name const & n) { return n == "a"; }
 inline expr mk_arrow(expr const & t, expr const & e) { return mk_pi(name("a"), t, e); }
 inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
 inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }
diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index 1f7badcb4..6cb8a8202 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -102,7 +102,7 @@ static name mk_unique_name(name_set & s, name const & suggestion) {
 std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const & ctx, expr const & t) {
     type_inferer inferer(env);
     if (!inferer.is_proposition(t, ctx))
-        throw exception("to_goal failed, type is not a proposition");
+        throw type_is_not_proposition_exception();
     name_set used_names = collect_used_names(ctx, t);
     buffer<context_entry> entries;
     for (auto const & e : ctx)
@@ -118,7 +118,7 @@ std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const
                 unsigned nvidx = vidx - offset;
                 unsigned nfv   = consts.size();
                 if (nvidx >= nfv)
-                    throw exception("to_goal failed, unknown free variable");
+                    throw exception("failed to create goal, unknown free variable");
                 unsigned lvl   = nfv - nvidx - 1;
                 if (bodies[lvl])
                     return *(bodies[lvl]);
diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h
index ab8e625ac..a0e226107 100644
--- a/src/library/tactic/goal.h
+++ b/src/library/tactic/goal.h
@@ -10,12 +10,22 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "util/list.h"
 #include "util/name.h"
+#include "util/exception.h"
 #include "kernel/formatter.h"
 #include "kernel/expr.h"
 #include "kernel/context.h"
 #include "kernel/environment.h"
 
 namespace lean {
+class type_is_not_proposition_exception : public exception {
+public:
+    type_is_not_proposition_exception() {}
+    virtual ~type_is_not_proposition_exception() noexcept {}
+    virtual char const * what() const noexcept { return "type is not a propostion"; }
+    virtual exception * clone() const { return new type_is_not_proposition_exception(); }
+    virtual void rethrow() const { throw *this; }
+};
+
 typedef std::pair<name, expr> hypothesis;
 typedef list<hypothesis>      hypotheses;
 class goal {
diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index 49ff65c13..658231eba 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/src/library/tactic/proof_state.cpp
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <utility>
 #include "util/sstream.h"
 #include "kernel/builtin.h"
+#include "kernel/type_checker.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/proof_state.h"
 
@@ -88,13 +90,27 @@ void proof_state::get_goal_names(name_set & r) const {
 
 static name g_main("main");
 
-proof_state to_proof_state(ro_environment const & env, context const & ctx, expr const & t) {
+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;
+        if (is_default_arrow_var_name(abst_name(t)) && is_proposition(abst_domain(t), env, ctx))
+            vname = name("H");
+        else
+            vname = abst_name(t);
+        extra_binders.emplace_front(vname, abst_domain(t));
+        ctx = extend(ctx, vname, abst_domain(t));
+        t   = abst_body(t);
+    }
     auto gfn                 = to_goal(env, ctx, t);
     goal g                   = gfn.first;
     goal_proof_fn fn         = gfn.second;
     proof_builder pr_builder = mk_proof_builder(
         [=](proof_map const & m, assignment const &) -> expr {
-            return fn(find(m, g_main));
+            expr pr = fn(find(m, g_main));
+            for (auto p : extra_binders)
+                pr = mk_lambda(p.first, p.second, pr);
+            return pr;
         });
     cex_builder cex_builder = mk_cex_builder_for(g_main);
     return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder);
diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h
index 524ecf16d..6ef79f656 100644
--- a/src/library/tactic/proof_state.h
+++ b/src/library/tactic/proof_state.h
@@ -96,7 +96,7 @@ public:
     format pp(formatter const & fmt, options const & opts) const;
 };
 
-proof_state to_proof_state(ro_environment const & env, context const & ctx, expr const & t);
+proof_state to_proof_state(ro_environment const & env, context ctx, expr t);
 
 inline optional<proof_state> some_proof_state(proof_state const & s, goals const & gs, proof_builder const & p) {
     return some(proof_state(s, gs, p));
diff --git a/tests/lean/pr1.lean b/tests/lean/pr1.lean
new file mode 100644
index 000000000..c360e15a5
--- /dev/null
+++ b/tests/lean/pr1.lean
@@ -0,0 +1,5 @@
+Theorem T (C A B : Bool) : C -> A -> B -> A.
+   assumption.
+   done.
+
+Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/pr1.lean.expected.out b/tests/lean/pr1.lean.expected.out
new file mode 100644
index 000000000..88791af06
--- /dev/null
+++ b/tests/lean/pr1.lean.expected.out
@@ -0,0 +1,4 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Proved: T
+Theorem T (C A B : Bool) (H : C) (H : A) (H::1 : B) : A := H