proposition: Lemma map_disjoint_list_to_map_zip_r {A} (m : M A) is xs : length is = length xs → m ##ₘ list_to_map (zip is xs) ↔ Forall (λ i, m !! i = None) is.
proof: Proof. intro. by rewrite (symmetry_iff map_disjoint), map_disjoint_list_to_map_zip_l. Qed.
imports: Coq(Permutation) stdpp(options)