simp only [Var.subst]
z : String
t : Var
i : ℕ
⊢ ((free_ z).subst t (bound_ i)).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
z : String
t : Var
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}