simp only [Var.boundVarSet] at a2
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ (free_ x).boundVarSet
⊢ v ∈ vs ∧ v.isBound
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
x : String
a2 : free_ x ∈ vs ∧ v ∈ ∅
⊢ v ∈ vs ∧ v.isBound