cases u
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
u : Var
a2 : u ∈ vs ∧ v ∈ u.freeVarSet
⊢ v ∈ vs ∧ v.isFree
case mpr.free_
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
a✝ : String
a2 : free_ a✝ ∈ vs ∧ v ∈ (free_ a✝).freeVarSet
⊢ v ∈ vs ∧ v.isFree

case mpr.bound_
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
a✝ : ℕ
a2 : bound_ a✝ ∈ vs ∧ v ∈ (bound_ a✝).freeVarSet
⊢ v ∈ vs ∧ v.isFree