proposition: Lemma lookup_mapset_map_with {A B} (f : bool → A → option B) X m i : mapset_map_with f X m !! i = m !! i ≫= f (bool_decide (i ∈ X)).
proof: Proof. destruct X as [mX]. unfold mapset_map_with, elem_of, mapset_elem_of. rewrite lookup_merge by done. simpl. by case_bool_decide; destruct (mX !! i) as [[]|], (m !! i). Qed.
imports: stdpp(options)