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