apply phi_ih
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
j : ℕ
⊢ (Formula.close j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet \ {free_ z}
no goals