diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 711604f91..7eb9c0d51 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -462,8 +462,19 @@ class elaborator {
             try {
                 bool no_info = true;
                 new_scope s(m_elab, m_state, no_info);
+                expr type = m_meta_type;
+                buffer<expr> locals;
+                while (is_pi(type)) {
+                    expr local  = ::lean::mk_local(m_elab.m_ngen.next(), binding_name(type), binding_domain(type),
+                                                   binding_info(type));
+                    if (binding_info(type).is_contextual())
+                        m_elab.m_context.add_local(local);
+                    m_elab.m_full_context.add_local(local);
+                    locals.push_back(local);
+                    type = instantiate(binding_body(type), local);
+                }
                 pair<expr, constraint_seq> rcs = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc.
-                expr r = rcs.first;
+                expr r = Fun(locals, rcs.first);
                 buffer<constraint> cs;
                 to_buffer(rcs.second, m_jst, cs);
                 return optional<constraints>(cons(mk_eq_cnstr(m_meta, r, m_jst, m_relax_main_opaque),
diff --git a/tests/lean/run/dfun_tst.lean b/tests/lean/run/dfun_tst.lean
new file mode 100644
index 000000000..15aea94af
--- /dev/null
+++ b/tests/lean/run/dfun_tst.lean
@@ -0,0 +1,10 @@
+import logic data.prod data.vector
+open prod nat inhabited vec
+
+theorem tst1 : inhabited (vec nat 2)
+
+theorem tst2 : inhabited (Prop × (Π n : nat, vec nat n))
+
+(*
+print(get_env():find("tst2"):value())
+*)