proposition: Lemma union_delete_insert {A} (m1 m2 : M A) i x : m1 !! i = Some x → delete i m1 ∪ <[i:=x]> m2 = m1 ∪ m2.
proof: Proof. intros. rewrite <-insert_union_r by apply lookup_delete. by rewrite insert_union_l, insert_delete by done. Qed.
imports: Coq(Permutation) stdpp(options)