simp only [Var.freeVarSet]
j : ℕ
zs : List String
x : String
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet ∪ (List.map free_ zs).toFinset
j : ℕ
zs : List String
x : String
⊢ {free_ x} ⊆ {free_ x} ∪ (List.map free_ zs).toFinset