proposition: Lemma elem_of_list_to_map {A} (l : list (K * A)) i x : NoDup (l.*1) → (i,x) ∈ l ↔ (list_to_map l : M A) !! i = Some x.
proof: Proof. split; auto using elem_of_list_to_map_1, elem_of_list_to_map_2. Qed.
imports: Coq(Permutation) stdpp(options)