trans Var.freeVarSet t ∪ Var.freeVarSet v \ {free_ z}
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ ((free_ z).subst t v).freeVarSet ⊆ t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}
z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ ((free_ z).subst t v).freeVarSet ⊆ t.freeVarSet ∪ v.freeVarSet \ {free_ z}

z : String
t : Var
X : String
vs : List Var
v : Var
a1 : v ∈ vs
⊢ t.freeVarSet ∪ v.freeVarSet \ {free_ z} ⊆ t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}