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