aesop
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
a : Char
aIn : a ∈ vocabOfFormula ϕ
⊢ a ∈ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula
no goals