induction h1
F : Formula
h1 : IsDeduct ∅ F
⊢ IsProofAlt F
case axiom_
F phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsProofAlt phi✝

case assume_
F phi✝ : Formula
a✝ : phi✝ ∈ ∅
⊢ IsProofAlt phi✝

case mp_
F phi✝ psi✝ : Formula
a✝¹ : IsDeduct ∅ (phi✝.imp_ psi✝)
a✝ : IsDeduct ∅ phi✝
a_ih✝¹ : IsProofAlt (phi✝.imp_ psi✝)
a_ih✝ : IsProofAlt phi✝
⊢ IsProofAlt psi✝