proposition: Lemma not_elem_of_list_to_map_1 {A} (l : list (K * A)) i : i ∉ l.*1 → (list_to_map l : M A) !! i = None.
proof: Proof. rewrite elem_of_list_fmap, eq_None_not_Some. intros Hi [x ?]; destruct Hi. exists (i,x); simpl; auto using elem_of_list_to_map_2. Qed.
imports: Coq(Permutation) stdpp(options)