apply IsReplOfFormulaInFormula.not_
case h1.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P).not_ (forall_ v P.not_.not_).not_
case h1.a.a.a.a.a
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ (forall_ v P) (forall_ v P.not_.not_)