trans v.freeVarSet ∪ (zs.map free_).toFinset
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.openList j (List.map free_ zs) v).freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ (Var.openList j (List.map free_ zs) v).freeVarSet ⊆ v.freeVarSet ∪ (List.map free_ zs).toFinset

zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ∪ (List.map free_ zs).toFinset ⊆ vs.toFinset.biUnion Var.freeVarSet ∪ (List.map free_ zs).toFinset