simp only [Var.freeVarSet]
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
⊢ (bound_ (i - j - (List.map free_ zs).length + j)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
⊢ ∅ ⊆ ∅ ∪ (List.map free_ zs).toFinset