simp only [Var.subst]
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (free_ x)).freeVarSet
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ (if free_ z = free_ x then t else free_ x).freeVarSet