simp only [Finset.union_right_comm S T {x}] at h1
v u : VarName
T : Finset VarName
h2 : v ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
S : Finset VarName
h1 : admitsAux v u (S ∪ T ∪ {x}) phi
⊢ admitsAux v u (S ∪ {x}) phi
v u : VarName
T : Finset VarName
h2 : v ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), admitsAux v u (S ∪ T) phi → admitsAux v u S phi
S : Finset VarName
h1 : admitsAux v u (S ∪ {x} ∪ T) phi
⊢ admitsAux v u (S ∪ {x}) phi