simp only [Formula.openList]
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) (phi.imp_ psi)).freeVarSet ⊆
    (phi.imp_ psi).freeVarSet ∪ (List.map free_ zs).toFinset
zs : List String
phi psi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
psi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) psi).freeVarSet ⊆ psi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ ((Formula.openList j (List.map free_ zs) phi).imp_ (Formula.openList j (List.map free_ zs) psi)).freeVarSet ⊆
    (phi.imp_ psi).freeVarSet ∪ (List.map free_ zs).toFinset