apply Finset.sdiff_subset_sdiff
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet \ {free_ z} ⊆ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
case hst
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ v.freeVarSet ⊆ vs.toFinset.biUnion Var.freeVarSet

case hvu
z X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
⊢ {free_ z} ⊆ {free_ z}