simp only [def_iff_]
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_ ((forall_ v P).iff_ (forall_ v P).not_.not_)
    ((forall_ v P).iff_ (forall_ v P.not_.not_).not_.not_)
case h1
P : Formula
v : VarName
⊢ IsReplOfFormulaInFormula P P.not_.not_
    (((forall_ v P).imp_ (forall_ v P).not_.not_).and_ ((forall_ v P).not_.not_.imp_ (forall_ v P)))
    (((forall_ v P).imp_ (forall_ v P.not_.not_).not_.not_).and_ ((forall_ v P.not_.not_).not_.not_.imp_ (forall_ v P)))