proposition: Lemma elem_of_list_to_map_1' {A} (l : list (K * A)) i x : (∀ y, (i,y) ∈ l → x = y) → (i,x) ∈ l → (list_to_map l : M A) !! i = Some x.
proof: Proof. induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|]. setoid_rewrite elem_of_cons. intros Hdup [?|?]; simplify_eq; [by rewrite lookup_insert|]. destruct (decide (i = j)) as [->|]. - rewrite lookup_insert; f_equal; eauto using eq_sym. - rewrite lookup_insert_ne by done; eauto. Qed.
imports: Coq(Permutation) stdpp(options)