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