title: Dealing with let-in expressions in current goal
body: <p>I got stuck while doing some coq proofs around the <code>state</code> monad. Concretely, I've simplified the situation to this proof:</p>
  
  <pre><code>Definition my_call {A B C} (f : A -&gt; B * C) (a : A) : B * C :=
    let (b, c) := f a in (b, c).
  
  Lemma mycall_is_call : forall {A B C} (f : A -&gt; B * C) (a : A), my_call f a = f a.
  Proof.
    intros A B C f a.
    unfold my_call.
    (* stuck! *)
  Abort.
  </code></pre>
  
  <p>The resulting goal after invoking <code>unfold</code> is <code>(let (b, c) := f a in (b, c)) = f a</code>. If I'm not wrong, both sides of the equality should be exactly the same, but I don't know how to show it from here. Any help?</p>
  
  <p>-- </p>
  
  <p>As a side note, I've seen that coq automatically applies the simplification when no product types are involved in the result of the function:</p>
  
  <pre><code>Definition my_call' {A B : Type} (f : A -&gt; B) (a : A) : B :=
    let b := f a in b.
  
  Lemma my_call_is_call' : forall A B (f : A -&gt; B) (a : A), my_call' f a = f a.
  Proof.
    intros A B f a.
    unfold my_call'.
    reflexivity.
  Qed.
  </code></pre>