proposition: Lemma union_singleton_r {A} (m : M A) i x y : m !! i = Some x → m ∪ {[i := y]} = m.
proof: Proof. intro Hlkup. apply map_eq. intros j. rewrite lookup_union. destruct (decide (i = j)); subst. - by rewrite !lookup_singleton, Hlkup. - rewrite lookup_singleton_ne by done. by destruct (m !! j). Qed.
imports: Coq(Permutation) stdpp(options)