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