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