How to prove theorem about list of pairs

I tried to continue proving this practice example that is about list of pairs, but it seems impossible. How should I continue to solve this theorem?

Require Import List.

Fixpoint split (A B:Set)(x:list (A*B)) : (list A)*(list B) :=
 match x with
   |nil => (nil, nil)
   |cons (a,b) x1 => 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) -> 
length y = length z.
Proof.
intros A 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 a b tx H y z.
simpl.
intro.
destruct (split A B tx).

Solution

Let me show you a couple of steps you can take to advance your proof. You have ended up in this proof state:

H0 : (a :: l, b :: l0) = (y, z)
============================
length y = length z

At this point it should be obvious that y and z are some non-empty lists. So injection H0. (or inversion H0. as suggested by Tej Chajed) helps you with this.

Then you can change your goal into

length l = length l0

using a combination of simplifications and rewrites (it depends on the exact tactic you use, inversion makes it simpler). You may also find the f_equal tactic very useful. At this point you are almost done because you can now use your induction hypothesis.