apply Exists.intro v
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isBound
⊢ ∃ a ∈ vs, v ∈ a.boundVarSet
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isBound
⊢ v ∈ vs ∧ v ∈ v.boundVarSet