case free_ x =>
  simp only [Var.openList]
  simp only [Var.freeVarSet]
  simp
j : ℕ
zs : List String
x : String
⊢ (Var.openList j (List.map free_ zs) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet ∪ (List.map free_ zs).toFinset
no goals