simp only [Formula.freeVarSet]
zs : List String
X : String
vs : List Var
j : ℕ
⊢ (pred_ X (List.map (Var.openList j (List.map free_ zs)) vs)).freeVarSet ⊆
    (pred_ X vs).freeVarSet ∪ (List.map free_ zs).toFinset
zs : List String
X : String
vs : List Var
j : ℕ
⊢ (List.map (Var.openList j (List.map free_ zs)) vs).toFinset.biUnion Var.freeVarSet ⊆
    vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset