simp only [Formula.freeVarSet]
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ (def_ a✝¹ a✝).freeVarSet
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ a✝.toFinset