. have s1 : ¬ u ∈ binders ∪ {x}
  exact Rec.fastAdmitsAux_isFreeIn phi v u (binders ∪ {x}) h1 c2
  simp at s1
  tauto
case pos.a
v u x : 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 ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ ¬x = u

case pos.a
v u x : 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 ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)
case pos.a
v u x : 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 ∪ {x}) phi
c1 : ¬v = x
c2 : isFreeIn v phi
⊢ IsSub phi v u (Rec.fastReplaceFree v u phi)