apply phi_ih
zs : List String
phi : Formula
phi_ih :
  ∀ (j : ℕ), (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
⊢ (Formula.openList j (List.map free_ zs) phi).freeVarSet ⊆ phi.freeVarSet ∪ (List.map free_ zs).toFinset
no goals