proposition: Theorem map_eq_if_all : forall (A B : Type)(ls : list A)(f1 f2 : A -> B), (forall a, In a ls -> f1 a = f2 a) -> map f1 ls = map f2 ls.
proof: Proof. induction ls; intuition; simpl in *. f_equal. eapply H. intuition. eapply IHls. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation