cases h <;> simp
case mp.cons
β : 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 ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ ∃ s ∈ head✝ :: tail✝, e ∈ s
case mp.cons.inl
β : 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 ∈ head✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a

case mp.cons.inr
β : 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 ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a