apply isFreeIn_imp_occursIn
case h.h1
v t : 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_right : ¬occursIn t phi
h1_left : t ≠ v
contra : isFreeIn t phi
⊢ occursIn t phi
case h.h1.h1
v t : 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_right : ¬occursIn t phi
h1_left : t ≠ v
contra : isFreeIn t phi
⊢ isFreeIn t phi