by_cases h : θ = ψ
case a.mp.intro.intro
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
case pos
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : θ = ψ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a

case neg
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
θ : Formula
left✝ : θ ∈ X
a_in_vocTheta : a✝ ∈ vocabOfFormula θ
h : ¬θ = ψ
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a