proposition: Lemma map_disjoint_list_to_map_l {A} (m : M A) ixs : list_to_map ixs ##ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
proof: Proof. split. - induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition. - induction 1; simpl; [apply map_disjoint_empty_l|]. rewrite map_disjoint_insert_l. auto. Qed.
imports: Coq(Permutation) stdpp(options)