tauto
F F' : Formula
v u : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ (Rec.fastReplaceFree h1_v h1_t h1_phi).not_ = h1_phi'.not_
no goals