proposition: Lemma foldr_delete_insert_ne {A} (m : M A) is j x : j ∉ is → foldr delete (<[j:=x]>m) is = <[j:=x]>(foldr delete m is).
proof: Proof. induction is as [|?? IHis]; simpl; [done |]. rewrite elem_of_cons. intros. rewrite IHis, delete_insert_ne; intuition. Qed.
imports: Coq(Permutation) stdpp(options)