proposition: Lemma map_disjoint_Some_l {A} (m1 m2 : M A) i x: m1 ##ₘ m2 → m1 !! i = Some x → m2 !! i = None.
proof: Proof. rewrite map_disjoint_spec, eq_None_not_Some. intros ?? [??]; eauto. Qed.
imports: Coq(Permutation) stdpp(options)