case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  cases h1
  case inl h1 =>
    apply mem_binders_imp_admitsAux
    subst h1
    simp
  case inr h1 =>
    apply phi_ih
    exact h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → admitsAux v u binders phi
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
⊢ admitsAux v u (binders ∪ {x}) phi
no goals