subst h1_ih_2
F F' : Formula
v u : VarName
h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_psi' : Formula
h1_2 : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_2 : Rec.fastReplaceFree h1_v h1_t h1_psi = h1_psi'
h1_1 : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi) =
    (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ h1_psi'
F F' : Formula
v u : VarName
h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_1 : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
h1_2 : IsSub h1_psi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_psi)
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi) =
    (Rec.fastReplaceFree h1_v h1_t h1_phi).iff_ (Rec.fastReplaceFree h1_v h1_t h1_psi)