induction l with
| nil => contradiction
| cons _ _ ih =>
  simp at h
  cases h <;> simp
  . apply Or.inl
    assumption
  . apply Or.inr
    apply ih
    assumption
case mp
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
h : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
⊢ ∃ s ∈ l, e ∈ s
no goals