proposition: Lemma map_fmap_omap {A B C} (f : A → option B) (g : B → C) (m : M A) : g <$> omap f m = omap (λ x, g <$> f x) m.
proof: Proof. apply map_eq. intros i. rewrite !lookup_fmap, !lookup_omap. destruct (m !! i); done. Qed.
imports: Coq(Permutation) stdpp(options)