simp only [Formula.close]
z X : String
vs : List Var
j : ℕ
⊢ (Formula.close j (free_ z) (pred_ X vs)).freeVarSet ⊆ (pred_ X vs).freeVarSet \ {free_ z}
z X : String
vs : List Var
j : ℕ
⊢ (pred_ X (List.map (Var.close j (free_ z)) vs)).freeVarSet ⊆ (pred_ X vs).freeVarSet \ {free_ z}