cases a_in
case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
a_in : (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a
case a.mpr.inl
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a

case a.mpr.inr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a