proposition: Lemma map_fmap_union {A B} (f : A → B) (m1 m2 : M A) : f <$> (m1 ∪ m2) = (f <$> m1) ∪ (f <$> m2).
proof: Proof. apply map_eq; intros i. apply option_eq; intros x. rewrite lookup_fmap, !lookup_union, !lookup_fmap. destruct (m1 !! i), (m2 !! i); auto. Qed.
imports: Coq(Permutation) stdpp(options)