case not_ phi phi_ih =>
  apply IsSub.not_
  exact phi_ih binders h1
v u : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), Rec.fastAdmitsAux v u binders phi → IsSub phi v u (Rec.fastReplaceFree v u phi)
binders : Finset VarName
h1 : Rec.fastAdmitsAux v u binders phi
⊢ IsSub phi.not_ v u (Rec.fastReplaceFree v u phi).not_
no goals