case _ i =>
  simp only [Var.freeVarSet] at a2
  simp at a2
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ (bound_ i).freeVarSet
⊢ v ∈ vs ∧ v.isFree
no goals