proposition: Theorem combine_map_eq : forall (A B C : Type)(lsa : list A)(lsb : list B)(f : B -> C), combine lsa (map f lsb) = map (fun p => (fst p, f (snd p))) (combine lsa lsb).
proof: Proof. induction lsa; destruct lsb; intuition; simpl in *. f_equal; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation