proposition: Lemma insert_singleton {A} i (x y : A) : <[i:=y]> {[i := x]} =@{M A} {[i := y]}.
proof: Proof. unfold singletonM, map_singleton, insert, map_insert. by rewrite <-partial_alter_compose. Qed.
imports: Coq(Permutation) stdpp(options)