case free_ x =>
  simp only [Var.close]
  split_ifs
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
  case _ c1 =>
    simp only [Var.freeVarSet]
    simp
    simp at c1
    exact c1
j : ℕ
z x : String
⊢ (Var.close j (free_ z) (free_ x)).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
no goals