rw [vocUnion]
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : voc {ϕ1, ϕ2} = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ1, ϕ2})
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : voc {ϕ1, ϕ2} = voc ψ
⊢ voc X = voc (X \ {ψ}) ∪ voc {ϕ1, ϕ2}