diff --git a/tests/lean/unfold_rec2.lean b/tests/lean/unfold_rec2.lean
new file mode 100644
index 000000000..421967b0b
--- /dev/null
+++ b/tests/lean/unfold_rec2.lean
@@ -0,0 +1,10 @@
+open nat
+
+definition f (a n : ℕ) : ℕ := nat.rec_on n (λa', a') (λn' f' a', f' (a' * 2)) a
+
+example (a n : nat) : a = 2 → f a (succ n) = f 4 n :=
+begin
+  unfold f at {1},
+  state,
+  intros, subst a
+end
diff --git a/tests/lean/unfold_rec2.lean.expected.out b/tests/lean/unfold_rec2.lean.expected.out
new file mode 100644
index 000000000..1ef368b97
--- /dev/null
+++ b/tests/lean/unfold_rec2.lean.expected.out
@@ -0,0 +1,3 @@
+unfold_rec2.lean:8:2: proof state
+a n : ℕ
+⊢ a = 2 → f (a * 2) n = f 4 n