use θ
case neg.h
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 θ
h : ¬θ = ψ
⊢ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
no goals