proposition: Lemma dom_imap_subseteq {A B} (f: K → A → option B) (m: M A) : dom (map_imap f m) ⊆ dom m.
proof: Proof. intros k. rewrite 2!elem_of_dom, map_lookup_imap. destruct 1 as [?[?[Eq _]]%bind_Some]. by eexists. Qed.
imports: stdpp(options)