test(tests/lean/unfold_rec2): add example from #692

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

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