proposition: Lemma elem_of_list_to_map_1 {A} (l : list (K * A)) i x : NoDup (l.*1) → (i,x) ∈ l → (list_to_map l : M A) !! i = Some x.
proof: Proof. intros ? Hx; apply elem_of_list_to_map_1'; eauto using NoDup_fmap_fst. intros y; revert Hx. rewrite !elem_of_list_lookup; intros [i' Hi'] [j' Hj']. cut (i' = j'); [naive_solver|]. apply NoDup_lookup with (l.*1) i; by rewrite ?list_lookup_fmap, ?Hi', ?Hj'. Qed.
imports: Coq(Permutation) stdpp(options)