rcases a_in with ⟨θ, theta_in_X, a_in_vocTheta⟩
case a.mp
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
a_in : ∃ a ∈ X, a✝ ∈ vocabOfFormula a
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
case a.mp.intro.intro
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
θ : Formula
theta_in_X : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
⊢ (∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a) ∨ a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2