proposition: Lemma combine_eq : forall {A B: Type} (l1a l2a: list A) (l1b l2b: list B), combine l1a l1b = combine l2a l2b -> length l1a = length l1b -> length l2a = length l2b -> l1a=l2a # l1b=l2b.
proof: Proof. induction l1a as [|a1 l1a Hind]; auto; introv Hc He1 He2; allsimpl; destruct l1b; destruct l2b; destruct l2a; try(invertsn He1); try(invertsn He2); allsimpl; try(invertsn Hc); auto. pose proof (Hind _ _ _ Hc He1 He2) as Xr. repnd. rewrite Xr. rewrite Xr0; split; sp. Qed.
imports: UsefulTypes bin_rels Omega