proposition: Lemma map_preimg_insert m i x : m !! i = None → map_preimg (<[i:=x]> m) = partial_alter (λ mX, Some ({[ i ]} ∪ default ∅ mX)) x (map_preimg m).
proof: Proof. intros Hi. refine (map_fold_insert_L _ _ i x m _ Hi). intros j1 j2 x1 x2 m' ? _ _. destruct (decide (x1 = x2)) as [->|?]. - rewrite <-!partial_alter_compose. apply partial_alter_ext; intros ? _; f_equal/=. set_solver. - by apply partial_alter_commute. Qed.
imports: Coq(Permutation) stdpp(options)