simp only [Formula.open]
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ (phi.imp_ psi).freeVarSet ⊆ (Formula.open j (free_ z) (phi.imp_ psi)).freeVarSet
z : String
phi psi : Formula
phi_ih : ∀ (j : ℕ), phi.freeVarSet ⊆ (Formula.open j (free_ z) phi).freeVarSet
psi_ih : ∀ (j : ℕ), psi.freeVarSet ⊆ (Formula.open j (free_ z) psi).freeVarSet
j : ℕ
⊢ (phi.imp_ psi).freeVarSet ⊆ ((Formula.open j (free_ z) phi).imp_ (Formula.open j (free_ z) psi)).freeVarSet