proposition: Lemma elem_of_map_to_set (f : K → A → B) (m : M A) (y : B) : y ∈ map_to_set (C:=C) f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y.
proof: Proof. unfold map_to_set; simpl. rewrite elem_of_list_to_set, elem_of_list_fmap. split. - intros ([i x] & ? & ?%elem_of_map_to_list); eauto. - intros (i&x&?&?). exists (i,x). by rewrite elem_of_map_to_list. Qed.
imports: Coq(Permutation) stdpp(options)