simp only [isFreeIn]
case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (def_ X✝ xs✝)
case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ v ∈ xs✝