simp only [Formula.freeVarSet]
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isFree ↔ v ∈ (pred_ X vs).freeVarSet
v : Var
X : String
vs : List Var
⊢ occursIn v (pred_ X vs) ∧ v.isFree ↔ v ∈ vs.toFinset.biUnion Var.freeVarSet