use ψ
case inl
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ