proposition: Theorem map_ne_same_ex : forall (A B : Set)(f1 f2 : A -> B)(ls : list A), eq_dec B -> map f1 ls <> map f2 ls -> exists a, In a ls /\ f1 a <> f2 a.
proof: Proof. induction ls; intuition; simpl in *. eapply cons_ne in H0. destruct H0. econstructor. intuition. intuition. destruct H2. intuition. exists x. intuition. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation