case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  apply phi_ih
  simp
  left
  exact h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → admitsAux v u binders phi
binders : Finset VarName
h1 : v ∈ binders
⊢ admitsAux v u (binders ∪ {x}) phi
no goals