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