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 =&gt; (3, 4)
    | _ =&gt; (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.