split_ifs
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi
case pos
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
h✝ : v = x
⊢ fastReplaceFree t v (exists_ x phi) = exists_ x phi

case neg
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
h✝ : ¬v = x
⊢ fastReplaceFree t v (exists_ x (fastReplaceFree v t phi)) = exists_ x phi