simp only [Var.freeVarSet]
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ (bound_ (i - 1)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ {free_ z}
j : ℕ
z : String
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ ∅ ⊆ ∅ ∪ {free_ z}