apply ih
case mp.cons.inr.h
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ ∃ a ∈ tail✝, e ∈ a
case mp.cons.inr.h
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝