simp at h1_1
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬(¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi)
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬h1_v = h1_x → ¬isFreeIn h1_v h1_phi
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi