DEFINITION or5_ind()
TYPE =
       ∀P0:Prop
         .∀P1:Prop
           .∀P2:Prop
             .∀P3:Prop
               .∀P4:Prop
                 .∀P:Prop
                   .P0→P
                     →(P1→P)→(P2→P)→(P3→P)→(P4→P)→(or5 P0 P1 P2 P3 P4)→P
BODY =
        assume P0: Prop
        assume P1: Prop
        assume P2: Prop
        assume P3: Prop
        assume P4: Prop
        assume P: Prop
        suppose H: P0→P
        suppose H1: P1→P
        suppose H2: P2→P
        suppose H3: P3→P
        suppose H4: P4→P
        suppose H5: or5 P0 P1 P2 P3 P4
          by cases on H5 we prove P
             case or5_intro0 H6:P0 ⇒
                the thesis becomes P
                by (H H6)
P
             case or5_intro1 H6:P1 ⇒
                the thesis becomes P
                by (H1 H6)
P
             case or5_intro2 H6:P2 ⇒
                the thesis becomes P
                by (H2 H6)
P
             case or5_intro3 H6:P3 ⇒
                the thesis becomes P
                by (H3 H6)
P
             case or5_intro4 H6:P4 ⇒
                the thesis becomes P
                by (H4 H6)
P
          we proved P
       we proved 
          ∀P0:Prop
            .∀P1:Prop
              .∀P2:Prop
                .∀P3:Prop
                  .∀P4:Prop
                    .∀P:Prop
                      .P0→P
                        →(P1→P)→(P2→P)→(P3→P)→(P4→P)→(or5 P0 P1 P2 P3 P4)→P