simp only [def_and_]
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).and_ ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)))
P : Formula
v : VarName
⊢ IsProof
    (((forall_ v P.not_).imp_ (forall_ v P.not_).not_.not_).imp_
        ((forall_ v P.not_).not_.not_.imp_ (forall_ v P.not_)).not_).not_