intro u a2
case mpr
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
⊢ ∀ (a : Var), a ∈ vs ∧ v ∈ a.freeVarSet → v ∈ vs ∧ v.isFree
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