induction h1
F : Formula
h1 : IsProofAlt F
⊢ IsDeduct ∅ F
case prop_true_
F : Formula
⊢ IsDeduct ∅ true_

case prop_1_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ (phi✝.imp_ (psi✝.imp_ phi✝))

case prop_2_
F phi✝ psi✝ chi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.imp_ (psi✝.imp_ chi✝)).imp_ ((phi✝.imp_ psi✝).imp_ (phi✝.imp_ chi✝)))

case prop_3_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.not_.imp_ psi✝.not_).imp_ (psi✝.imp_ phi✝))

case pred_1_
F : Formula
v✝ : VarName
phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((forall_ v✝ (phi✝.imp_ psi✝)).imp_ ((forall_ v✝ phi✝).imp_ (forall_ v✝ psi✝)))

case pred_2_
F : Formula
v✝ t✝ : VarName
phi✝ phi'✝ : Formula
a✝¹ : fastAdmits v✝ t✝ phi✝
a✝ : fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ IsDeduct ∅ ((forall_ v✝ phi✝).imp_ phi'✝)

case pred_3_
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : ¬isFreeIn v✝ phi✝
⊢ IsDeduct ∅ (phi✝.imp_ (forall_ v✝ phi✝))

case eq_1_
F : Formula
v✝ : VarName
⊢ IsDeduct ∅ (forall_ v✝ (eq_ v✝ v✝))

case eq_2_pred_const_
F : Formula
name✝ : PredName
n✝ : ℕ
xs✝ ys✝ : Fin n✝ → VarName
⊢ IsDeduct ∅
    (Forall_ (List.ofFn xs✝)
      (Forall_ (List.ofFn ys✝)
        ((And_ (List.ofFn fun i => eq_ (xs✝ i) (ys✝ i))).imp_
          ((pred_const_ name✝ (List.ofFn xs✝)).iff_ (pred_const_ name✝ (List.ofFn ys✝))))))

case eq_2_eq_
F : Formula
x_0✝ x_1✝ y_0✝ y_1✝ : VarName
⊢ IsDeduct ∅
    (forall_ x_0✝
      (forall_ x_1✝
        (forall_ y_0✝
          (forall_ y_1✝ (((eq_ x_0✝ y_0✝).and_ (eq_ x_1✝ y_1✝)).imp_ ((eq_ x_0✝ x_1✝).iff_ (eq_ y_0✝ y_1✝)))))))

case gen_
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : IsProofAlt phi✝
a_ih✝ : IsDeduct ∅ phi✝
⊢ IsDeduct ∅ (forall_ v✝ phi✝)

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

case def_false_
F : Formula
⊢ IsDeduct ∅ (false_.iff_ true_.not_)

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

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

case def_iff_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅
    (((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 : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsDeduct ∅ ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)