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
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
no goals