. intro ⟨x, h₁, h₂⟩
  have ⟨s, _⟩ := s
  revert s
  apply Quot.ind
  intro l _ h
  simp [Finset.fold, Multiset.fold]
  apply List.mem_fold_union_iff.mpr
  exists f x
  simp; constructor
  exists x
  assumption
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ (∃ x ∈ s, e ∈ f x) → e ∈ fold Union.union ∅ f s
no goals