case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    apply phi_ih (binders ∪ {x}) h1_right
    simp
    tauto
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → admitsAux v u binders phi
binders : Finset VarName
h1 : ¬(u = x ∨ isBoundIn u phi)
h2 : u ∉ binders
⊢ admitsAux v u (binders ∪ {x}) phi
no goals