case _ x =>
  simp only [Var.freeVarSet] at a2
  simp at a2
  cases a2
  case _ a2_left a2_right =>
    subst a2_right
    simp only [isFree]
    simp
    exact a2_left
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ (free_ x).freeVarSet
⊢ v ∈ vs ∧ v.isFree
no goals