proposition: Lemma combine_split : forall (l:list A)(l':list B), length l = length l' -> split (combine l l') = (l,l').
proof: Proof. intro l; induction l as [|a l IHl]; intro l'; destruct l'; simpl; trivial; try discriminate. now intros [= ->%IHl]. Qed.
imports: PeanoNat