case prop_2_ h1_1_phi h1_1_psi h1_1_chi =>
  apply IsProofAlt.prop_2_
F h1_phi h1_1_phi h1_1_psi h1_1_chi : Formula
⊢ IsProofAlt ((h1_1_phi.imp_ (h1_1_psi.imp_ h1_1_chi)).imp_ ((h1_1_phi.imp_ h1_1_psi).imp_ (h1_1_phi.imp_ h1_1_chi)))
no goals