Obsługa pozwól w hipotezie

Question

Jako ćwiczenie w Coq, próbuję udowodnić, że następująca funkcja zwraca parę list o jednakowej długości.

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. 

Po ostatnim kroku dostaję hipotezę o let rachunku środka, który nie wiem jak obsługiwać:

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) -> 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 

Answer 1

Chcesz zrobić destruct (split A B tx). Spowoduje to przerwanie, wiążąc obie części z i