apply Rec.not_free_in_fastReplaceFree_self
case h.e'_2
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
c1 : ¬h1_v = h1_x
⊢ Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi
case h.e'_2.h1
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
c1 : ¬h1_v = h1_x
⊢ ¬isFreeIn h1_v h1_phi