subst a2_right
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.freeVarSet
x : String
a2_left : free_ x ∈ vs
a2_right : v = free_ x
⊢ v ∈ vs ∧ v.isFree
X : String
vs : List Var
x : String
a2_left : free_ x ∈ vs
a1 : ∃ a ∈ vs, free_ x ∈ a.freeVarSet
⊢ free_ x ∈ vs ∧ (free_ x).isFree