proposition: Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
proof: Proof. split. - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|]. setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver. - intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |]. intros. apply elem_of_union_r; auto. Qed.
imports: stdpp(finite) stdpp(options)