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