proposition: Lemma map_disjoint_list_to_map_r {A} (m : M A) ixs : m ##ₘ list_to_map ixs ↔ Forall (λ ix, m !! ix.1 = None) ixs.
proof: Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_list_to_map_l. Qed.
imports: Coq(Permutation) stdpp(options)