simp at a2
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v ∈ {bound_ i}
⊢ v ∈ vs ∧ v.isBound
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
a2 : bound_ i ∈ vs ∧ v = bound_ i
⊢ v ∈ vs ∧ v.isBound