proposition: Lemma kmap_omap {A B} (g : A → option B) (m : M1 A) : kmap f (omap g m) = omap g (kmap f m).
proof: Proof. apply map_eq; intros j. apply option_eq; intros y. rewrite lookup_omap, bind_Some. setoid_rewrite lookup_kmap_Some. setoid_rewrite lookup_omap. setoid_rewrite bind_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)