proposition: Lemma elem_of_list_to_map_2 {A} (l : list (K * A)) i x : (list_to_map l : M A) !! i = Some x → (i,x) ∈ l.
proof: Proof. induction l as [|[j y] l IH]; simpl; [by rewrite lookup_empty|]. rewrite elem_of_cons. destruct (decide (i = j)) as [->|]; rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. Qed.
imports: Coq(Permutation) stdpp(options)