proposition: Lemma not_elem_of_list_to_map {A} (l : list (K * A)) i : i ∉ l.*1 ↔ (list_to_map l : M A) !! i = None.
proof: Proof. red; auto using not_elem_of_list_to_map_1,not_elem_of_list_to_map_2. Qed.
imports: Coq(Permutation) stdpp(options)