simp only [isFreeIn] at h1
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isFreeIn v (def_ a✝¹ a✝)
⊢ occursIn v (def_ a✝¹ a✝)
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ occursIn v (def_ a✝¹ a✝)