all_goals
  sorry
case def_false_
F h1_phi : Formula
⊢ IsProofAlt (false_.iff_ true_.not_)

case def_and_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt
    (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
        (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
F h1_phi : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsProofAlt ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
no goals