Processing allowed in hypothesis

Question

As an exercise in Coq, I am trying to prove that the following function returns a pair of lists of the same length.

Require Import List. Fixpoint split (AB:Set)(x:list (A*B)) : (list A)*(list B) := match x with |nil => (nil, nil) |cons (a,b) x1 => let (ta, tb) := split AB x1 in (a::ta, b::tb) end. Theorem split_eq_len : forall (AB:Set)(x:list (A*B))(y:list A)(z:list B),(split AB x)=(y,z) -> length y = length z. Proof. intros AB x. elim x. simpl. intros y z. intros H. injection H. intros H1 H2. rewrite <- H1. rewrite <- H2. reflexivity. intros hx. elim hx. intros ab tx H y z. simpl. intro. 

After the last step, I get a hypothesis with a let statement inside that I don't know how to handle:

 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 AB tx = (y, z) -> length y = length z y : list A z : list B H0 : (let (ta, tb) := split AB tx in (a :: ta, b :: tb)) = (y, z) ______________________________________(1/1) length y = length z 

Answer 1

You want to do destruct (split AB tx) . This will break it by tying two parts to ta and tb