coq - Handling let in hypothesis -

as exercise in coq, i'm trying prove following function returns pair of lists of equal length.

require import list.  fixpoint split (a b:set)(x:list (a*b)) : (list a)*(list b) := match x |nil => (nil, nil) |cons (a,b) x1 => let (ta, tb) := split 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 b x)=(y,z) -> length y = length z. proof. intros b x. elim x. simpl. intros y z. intros h. injection h. intros h1 h2. rewrite <- h1. rewrite <- h2. reflexivity. intros hx. elim hx. intros b tx h y z. simpl. intro. 

after last step hypothesis let statement inside, not know how handle:

1 subgoals : set b : set x : list (a * b) hx : * b : b : b tx : list (a * b) h : forall (y : list a) (z : list b),     split b tx = (y, z) -> length y = length z y : list z : list b h0 : (let (ta, tb) := split b tx in (a :: ta, b :: tb)) = (y, z) ______________________________________(1/1) length y = length z 

you want destruct (split b tx). break up, binding 2 pieces ta , tb