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