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