simp at *
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : voc ϕ = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ})
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
⊢ X.biUnion vocabOfFormula = vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula