simp only [Var.close]
j : ℕ
z : String
i : ℕ
⊢ (Var.close j (free_ z) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}
j : ℕ
z : String
i : ℕ
⊢ (if i < j then bound_ i else bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}