title: Handling let in hypothesis
body: <p>As an exercise in Coq, I'm trying to prove that the following function returns a pair of lists of equal length.</p>
  
  <pre><code>Require Import List.
  
  Fixpoint split (A B:Set)(x:list (A*B)) : (list A)*(list B) :=
  match x with
  |nil =&gt; (nil, nil)
  |cons (a,b) x1 =&gt; let (ta, tb) := split A B x1 in (a::ta, b::tb)
  end.
  
  Theorem split_eq_len : forall (A B:Set)(x:list (A*B))(y:list A)(z:list B),(split A B x)=(y,z) -&gt; length y = length z.
  Proof.
  intros A B x.
  elim x.
  simpl.
  intros y z.
  intros H.
  injection H.
  intros H1 H2.
  rewrite &lt;- H1.
  rewrite &lt;- H2.
  reflexivity.
  intros hx.
  elim hx.
  intros a b tx H y z.
  simpl.
  intro.
  </code></pre>
  
  <p>After the last step I get a hypothesis with a <code>let</code> statement inside, which I do not know how to handle:</p>
  
  <pre><code>1 subgoals
  A : Set
  B : Set
  x : list (A * B)
  hx : A * B
  a : A
  b : B
  tx : list (A * B)
  H : forall (y : list A) (z : list B),
      split A B tx = (y, z) -&gt; length y = length z
  y : list A
  z : list B
  H0 : (let (ta, tb) := split A B tx in (a :: ta, b :: tb)) = (y, z)
  ______________________________________(1/1)
  length y = length z
  </code></pre>