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

case h.hvu
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs.toFinset
⊢ {free_ z} ⊆ {free_ z}