DEFINITION or4_ind()
TYPE =
       ∀P0:Prop
         .∀P1:Prop
           .∀P2:Prop
             .∀P3:Prop
               .∀P:Prop
                 .(P0→P)→(P1→P)→(P2→P)→(P3→P)→(or4 P0 P1 P2 P3)→P
BODY =
        assume P0: Prop
        assume P1: Prop
        assume P2: Prop
        assume P3: Prop
        assume P: Prop
        suppose H: P0→P
        suppose H1: P1→P
        suppose H2: P2→P
        suppose H3: P3→P
        suppose H4: or4 P0 P1 P2 P3
          by cases on H4 we prove P
             case or4_intro0 H5:P0 ⇒
                the thesis becomes P
                by (H H5)
P
             case or4_intro1 H5:P1 ⇒
                the thesis becomes P
                by (H1 H5)
P
             case or4_intro2 H5:P2 ⇒
                the thesis becomes P
                by (H2 H5)
P
             case or4_intro3 H5:P3 ⇒
                the thesis becomes P
                by (H3 H5)
P
          we proved P
       we proved 
          ∀P0:Prop
            .∀P1:Prop
              .∀P2:Prop
                .∀P3:Prop
                  .∀P:Prop
                    .(P0→P)→(P1→P)→(P2→P)→(P3→P)→(or4 P0 P1 P2 P3)→P