case inl h1 =>
  apply mem_binders_imp_admitsAux
  subst h1
  simp
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
⊢ admitsAux v u (binders ∪ {x}) phi
no goals