norm_num at *
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a ∈ X.biUnion vocabOfFormula
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : vocabOfFormula ϕ ⊆ vocabOfFormula ψ
a : Char
a_in : a ∈ vocabOfFormula ϕ ∨ ∃ a_1, (¬a_1 = ψ ∧ a_1 ∈ X) ∧ a ∈ vocabOfFormula a_1
⊢ ∃ a_1 ∈ X, a ∈ vocabOfFormula a_1