simp only [Var.open]
j : ℕ
z : String
i : ℕ
⊢ (Var.open j (free_ z) (bound_ i)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ {free_ z}
j : ℕ
z : String
i : ℕ
⊢ (if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ {free_ z}