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