proposition: Theorem map_eq_subset : forall (A B : Type)(ls2 ls1 : list A)(f1 f2 : A -> B), map f1 ls1 = map f2 ls1 -> (forall a, In a ls2 -> In a ls1) -> map f1 ls2 = map f2 ls2.
proof: Proof. intuition. specialize (map_eq_all _ _ _ H); intros. eapply map_eq_if_all. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation