case _ x =>
  simp only [Var.freeVarSet]
  simp
  cases a1
  case _ a1_left a1_right =>
    exact a1_left
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).freeVarSet
no goals