cases a2
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2 : free_ x ∈ vs ∧ v = free_ x
⊢ v ∈ vs ∧ v.isFree
case intro
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
left✝ : free_ x ∈ vs
right✝ : v = free_ x
⊢ v ∈ vs ∧ v.isFree