proposition: Lemma elem_of_list_to_set (x : A) l : x ∈ list_to_set (C:=C) l ↔ x ∈ l.
proof: Proof. split. - induction l; simpl; [by rewrite elem_of_empty|]. rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto. - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto. Qed.
imports: stdpp(finite) stdpp(options)