case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  cases h1
  case inl h1 =>
    tauto
  case inr h1 =>
    specialize phi_ih (S ∪ {x}) h1
    right
    simp only [Finset.union_right_comm_assoc]
    exact phi_ih
v u : VarName
T : Finset VarName
h2 : u ∉ T
x : VarName
phi : Formula
phi_ih : ∀ (S : Finset VarName), fastAdmitsAux v u S phi → fastAdmitsAux v u (S ∪ T) phi
S : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (S ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (S ∪ T ∪ {x}) phi
no goals