simp only [isFreeIn]
case a
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
c1 : ¬v = v
⊢ ¬isFreeIn v (exists_ v phi)
case a
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
c1 : ¬v = v
⊢ ¬(¬True ∧ isFreeIn v phi)