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