case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    split_ifs
    case pos c1 =>
      simp only [fastAdmitsAux]
      subst c1
      right
      apply not_isFreeIn_imp_fastAdmitsAux
      intro contra
      apply h1_right
      apply isFreeIn_imp_occursIn
      exact contra
    case neg c1 =>
      simp only [fastAdmitsAux]
      right
      apply phi_ih (binders ∪ {x}) h1_right
      simp
      tauto
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h1 : ¬(t = x ∨ occursIn t phi)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
no goals