proposition: Theorem Forall2_map_eq : forall (A B C : Type)(f1 : A -> C)(f2 : B -> C)(lsa : list A)(lsb : list B), Forall2 (fun a b => f1 a = f2 b) lsa lsb -> map f1 lsa = map f2 lsb.
proof: Proof. induction 1; intuition idtac; simpl in *. f_equal. trivial. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation