proposition: Lemma not_elem_of_list_to_map_2 {A} (l : list (K * A)) i : (list_to_map l : M A) !! i = None → i ∉ l.*1.
proof: Proof. induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|]. rewrite elem_of_cons. destruct (decide (i = j)); simplify_eq. - by rewrite lookup_insert. - by rewrite lookup_insert_ne; intuition. Qed.
imports: Coq(Permutation) stdpp(options)