simp only [Var.freeVarSet]
j : ℕ
zs : List String
i : ℕ
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
⊢ (free_ (zs.get ⟨i - 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
⊢ {free_ (zs.get ⟨i - j, ⋯⟩)} ⊆ ∅ ∪ (List.map free_ zs).toFinset