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