case axiom_ h1_phi h1_1 =>
  induction h1_1
  case prop_true_ =>
    apply IsProofAlt.prop_true_
  case prop_1_ h1_1_phi h1_1_psi =>
    apply IsProofAlt.prop_1_
  case prop_2_ h1_1_phi h1_1_psi h1_1_chi =>
    apply IsProofAlt.prop_2_
  case prop_3_ h1_1_phi h1_1_psi =>
    apply IsProofAlt.prop_3_
  case pred_1_ h1_1_v h1_1_phi h1_1_psi =>
    apply IsProofAlt.pred_1_
  case pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2 =>
    apply IsProofAlt.pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2
  case pred_3_ h1_1_v h1_1_phi h1_1_1 =>
    apply IsProofAlt.pred_3_
    exact h1_1_1
  case eq_1_ h1_1 =>
    apply IsProofAlt.eq_1_
  case eq_2_pred_const_ h1_1_name h1_1_n h1_1_xs h1_1_ys =>
    apply IsProofAlt.eq_2_pred_const_
  case eq_2_eq_ h1_1_x_0 h1_1_y_0 h1_1_x_1 h1_1_y_1 =>
    apply IsProofAlt.eq_2_eq_
  case gen_ h1_1_v h1_1_phi h1_1_1 h1_1_ih =>
    apply IsProofAlt.gen_
    exact h1_1_ih
  all_goals
    sorry
F h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsProofAlt h1_phi
no goals