diff --git a/src/library/blast/intros_action.cpp b/src/library/blast/intros_action.cpp
index d8793a43c..1ef5da72a 100644
--- a/src/library/blast/intros_action.cpp
+++ b/src/library/blast/intros_action.cpp
@@ -37,10 +37,11 @@ bool intros_action(unsigned max) {
         if (!is_pi(target))
             break;
         expr href;
+        expr htype = head_beta_reduce(binding_domain(target));
         if (is_default_var_name(binding_name(target)) && closed(binding_body(target))) {
-            href  = s.mk_hypothesis(binding_domain(target));
+            href  = s.mk_hypothesis(htype);
         } else {
-            href  = s.mk_hypothesis(binding_name(target), binding_domain(target));
+            href  = s.mk_hypothesis(binding_name(target), htype);
         }
         new_hs.push_back(href);
         target     = whnf(instantiate(binding_body(target), href));
diff --git a/tests/lean/run/blast15.lean b/tests/lean/run/blast15.lean
new file mode 100644
index 000000000..89f704e66
--- /dev/null
+++ b/tests/lean/run/blast15.lean
@@ -0,0 +1,4 @@
+definition lemma1 (p : nat → Prop) (q : nat → nat → Prop) : (∃ x y, p x ∧ q x y) → q 0 0 ∧ q 1 1 → (∃ x, p x) :=
+by blast
+
+print lemma1