subst h1_ih
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
⊢ 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
a✝¹ : ¬h1_x = h1_t
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
a✝ : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
⊢ exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi) = exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)