DEFINITION and5_ind()
TYPE =
       ∀P0:Prop
         .∀P1:Prop
           .∀P2:Prop
             .∀P3:Prop.∀P4:Prop.∀P:Prop.(P0→P1→P2→P3→P4→P)→(and5 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→P1→P2→P3→P4→P
        suppose H1: and5 P0 P1 P2 P3 P4
          by cases on H1 we prove P
             case and5_intro H2:P0 H3:P1 H4:P2 H5:P3 H6:P4 ⇒
                the thesis becomes P
                by (H H2 H3 H4 H5 H6)
P
          we proved P
       we proved 
          ∀P0:Prop
            .∀P1:Prop
              .∀P2:Prop
                .∀P3:Prop.∀P4:Prop.∀P:Prop.(P0→P1→P2→P3→P4→P)→(and5 P0 P1 P2 P3 P4)→P