apply Exists.elim a1
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
⊢ v ∈ vs ∧ v.isBound
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
⊢ ∀ (a : Var), a ∈ vs ∧ v ∈ a.boundVarSet → v ∈ vs ∧ v.isBound