simp only [Var.freeVarSet]
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).freeVarSet
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs ∧ free_ x ∈ {free_ x}