proposition: Lemma lookup_set_to_map (f : B → K * A) (Y : C) i x : (∀ y y', y ∈ Y → y' ∈ Y → (f y).1 = (f y').1 → y = y') → (set_to_map f Y : M A) !! i = Some x ↔ ∃ y, y ∈ Y ∧ f y = (i,x).
proof: Proof. intros Hinj. assert (∀ x', (i, x) ∈ f <$> elements Y → (i, x') ∈ f <$> elements Y → x = x'). { intros x'. intros (y&Hx&Hy)%elem_of_list_fmap (y'&Hx'&Hy')%elem_of_list_fmap. rewrite elem_of_elements in Hy, Hy'. cut (y = y'); [congruence|]. apply Hinj; auto. by rewrite <-Hx, <-Hx'. } unfold set_to_map; rewrite <-elem_of_list_to_map' by done. rewrite elem_of_list_fmap. setoid_rewrite elem_of_elements; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)