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_left : free_ x ∈ vs
a2_right : v = free_ x
⊢ v ∈ vs ∧ v.isFree
no goals