Proof of equality with destructuring let...in

I have some expression (f n in the example below) returning a tuple. I would like to prove that f n is equal to let (x, y) := f n in (x, y), which seems like it should be easy. What tactic should I use?

Definition f (n : nat) : nat * nat :=
  match n with
    | 0 => (3, 4)
    | _ => (2, 3)
  end.
Lemma foo : forall n, f n = (let (x, y) := f n in (x, y)).
  auto. (*doesn't do anything*)
  destruct n.
  auto.
  auto.
Qed.

The same task with let tup := f n in tup can be done with the tactic trivial. The same task with both f n replaced by an explicit tuple (f n, 12) is also covered by trivial. Here I had to destruct n (or do a pointless induction n) to make the "tupleness" of f n be manifest.

You can destruct not only on variables, but on expressions like f n as well. So, this will get you a solution:

Lemma foo : forall n, f n = (let (x, y) := f n in (x, y)).
  intro n.
  now destruct (f n).    (* or destruct (f n). reflexivity. *)
Qed.

StackExchange Computer Science Q#63391, answer score: 7