apply C_18_4 P P.not_.not_ ((forall_ v P).iff_ (forall_ v P).not_.not_)
P : Formula
v : VarName
⊢ IsProof ((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).iff_ (forall_ v P).not_.not_)
    ((forall_ v P).iff_ (forall_ v P.not_.not_).not_.not_)

case h2
P : Formula
v : VarName
⊢ IsProof (P.iff_ P.not_.not_)

case h3
P : Formula
v : VarName
⊢ IsDeduct ∅ ((forall_ v P).iff_ (forall_ v P).not_.not_)