simp at *
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
psi_in_insert : ϕ ∈ insert ψ S
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
⊢ vocabOfFormula ϕ ⊆ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula