simp only [isBoundIn]
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isBoundIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).boundVarSet
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ v ∈ (def_ a✝¹ a✝).boundVarSet