simp only [Formula.open]
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.open j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet ∪ {free_ z}
j : ℕ
⊢ (Formula.open j (free_ z) phi.not_).freeVarSet ⊆ phi.not_.freeVarSet ∪ {free_ z}
z : String
phi : Formula
phi_ih : ∀ (j : ℕ), (Formula.open j (free_ z) phi).freeVarSet ⊆ phi.freeVarSet ∪ {free_ z}
j : ℕ
⊢ (Formula.open j (free_ z) phi).not_.freeVarSet ⊆ phi.not_.freeVarSet ∪ {free_ z}