proposition: Lemma map_eq_inv : forall (A B : Set)(f1 f2 : A -> B)(ls : list A), map f1 ls = map f2 ls -> forall a, In a ls -> f1 a = f2 a.
proof: Proof. induction ls; intuition; simpl in *; intuition. subst. inversion H; clear H; subst. trivial. inversion H; clear H; subst. eauto. Qed.
imports: FCF.FCF Permutation