proposition: Lemma map_combine : forall {T1 T2 T3 T4} (f: T1 -> T3) (g: T2 -> T4) (l1: list T1) (l2: list T2), map (fun x => (f (fst x), g (snd x))) (combine l1 l2) = combine (map f l1) (map g l2).
proof: Proof. Proof. induction l1 as [| h1 l1 Hind]; intros; allsimpl; auto;[]. destruct l2; auto;[]. simpl. f_equal; auto. Qed.
imports: UsefulTypes bin_rels Omega