proposition: Theorem map_ext_in : forall (A B : Set)(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. eauto. Qed.
imports: FCF.FCF Permutation