cases h1
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 ∨ Rec.fastAdmitsAux v u (binders ∪ {x}) phi
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))
case inl
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
h✝ : v = x
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))

case inr
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
h✝ : Rec.fastAdmitsAux v u (binders ∪ {x}) phi
⊢ IsSub (exists_ x phi) v u (if v = x then exists_ x phi else exists_ x (Rec.fastReplaceFree v u phi))