simp at h
case mpr.cons
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s ∈ head✝ :: tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ (head✝ :: tail✝)
case mpr.cons
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝ ∨ s ∈ tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ (head✝ :: tail✝)