intro psi_in_X eq_voc
X : Finset Formula
ψ ϕ : Formula
⊢ ψ ∈ X → voc ϕ = voc ψ → voc X = voc (X \ {ψ} ∪ {ϕ})
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : voc ϕ = voc ψ
⊢ voc X = voc (X \ {ψ} ∪ {ϕ})