proposition: Lemma insert_id {A} (m : M A) i x : m !! i = Some x → <[i:=x]>m = m.
proof: Proof. intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|]; by rewrite ?lookup_insert, ?lookup_insert_ne by done. Qed.
imports: Coq(Permutation) stdpp(options)