simp only [Finset.mem_union]
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → u ∉ S ∪ T
case def_
v u : VarName
T : Finset VarName
h2 : u ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ → u ∉ S
⊢ v ∈ a✝ → ¬(u ∈ S ∨ u ∈ T)