apply IsSub.exists_not_free_in
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 : v = x
c1 : ¬v = x
⊢ IsSub (exists_ x phi) v u (exists_ x phi)
case 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 : v = x
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x phi)