proposition: Lemma map_disjoint_insert_r {A} (m1 m2 : M A) i x : m1 ##ₘ <[i:=x]>m2 ↔ m1 !! i = None ∧ m1 ##ₘ m2.
proof: Proof. rewrite insert_union_singleton_l. by rewrite map_disjoint_union_r, map_disjoint_singleton_r. Qed.
imports: Coq(Permutation) stdpp(options)