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