. have ⟨s, _⟩ := s
  revert s
  apply Quot.ind
  intro l _ h
  dsimp [Finset.fold] at h
  have ⟨_, h, _⟩ := List.mem_fold_union_iff.mp h
  simp at h
  have ⟨x, _, h⟩ := h
  exists x; simp [h]
  constructor; repeat { assumption }
case mp
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ e ∈ fold Union.union ∅ f s → ∃ x ∈ s, e ∈ f x

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
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