cases v
case mp
v : Var
X : String
vs : List Var
a1 : v ∈ vs ∧ v.isBound
⊢ v ∈ vs ∧ v ∈ v.boundVarSet
case mp.free_
X : String
vs : List Var
a✝ : String
a1 : free_ a✝ ∈ vs ∧ (free_ a✝).isBound
⊢ free_ a✝ ∈ vs ∧ free_ a✝ ∈ (free_ a✝).boundVarSet

case mp.bound_
X : String
vs : List Var
a✝ : ℕ
a1 : bound_ a✝ ∈ vs ∧ (bound_ a✝).isBound
⊢ bound_ a✝ ∈ vs ∧ bound_ a✝ ∈ (bound_ a✝).boundVarSet