intro v a1
z X : String
vs : List Var
j : ℕ
⊢ ∀ x ∈ vs, x.freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ (List.map (Var.open j (free_ z)) vs).toFinset.biUnion Var.freeVarSet