proposition: Lemma map_disjoint_list_to_map_zip_l {A} (m : M A) is xs : length is = length xs → list_to_map (zip is xs) ##ₘ m ↔ Forall (λ i, m !! i = None) is.
proof: Proof. intro. rewrite map_disjoint_list_to_map_l. rewrite <-(fst_zip is xs) at 2 by lia. by rewrite Forall_fmap. Qed.
imports: Coq(Permutation) stdpp(options)