simp only [admitsAux] at h1
case def_
v u : VarName
T : Finset VarName
h2 : v ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : admitsAux v u (S ∪ T) (def_ a✝¹ a✝)
⊢ admitsAux v u S (def_ a✝¹ a✝)
case def_
v u : VarName
T : Finset VarName
h2 : v ∉ T
a✝¹ : DefName
a✝ : List VarName
S : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ S ∪ T → u ∉ S ∪ T
⊢ admitsAux v u S (def_ a✝¹ a✝)