proposition: Lemma split_length_eq: forall {A B :Type} (sub : list (A * B)), let (la,lb):= split sub in length la=length lb # length la= length sub.
proof: Proof. intros. destructr (split sub) as [la lb]. assert(la=fst (la,lb)) as h99 by (simpl;auto). rewrite h99. rewrite HeqHdeq. rewrite split_length_l. clear h99. assert(lb=snd (la,lb)) as h99 by (simpl;auto). rewrite h99. rewrite HeqHdeq. rewrite split_length_r. sp. Qed.
imports: UsefulTypes bin_rels Omega