proposition: Lemma map_omap_map_compose `{FinMap A MA, FinMap B MB} {C1 C2} (f : C1 → option C2) (m : MB C1) (n : MA B) : omap f (m ∘ₘ n) = omap f m ∘ₘ n.
proof: Proof. apply map_eq; intros a. rewrite lookup_omap, !map_lookup_compose. destruct (n !! a); simpl; [|done]. by rewrite lookup_omap. Qed.
imports: Coq(Permutation) stdpp(options)