DEFINITION ex5_3_ind()
TYPE =
       ∀A0:Set
         .∀A1:Set
           .∀A2:Set
             .∀P0:A0→A1→A2→Prop
               .∀P1:A0→A1→A2→Prop
                 .∀P2:A0→A1→A2→Prop
                   .∀P3:A0→A1→A2→Prop
                     .∀P4:A0→A1→A2→Prop
                       .∀P:Prop
                         .∀a:A0.∀a1:A1.∀a2:A2.(P0 a a1 a2)→(P1 a a1 a2)→(P2 a a1 a2)→(P3 a a1 a2)→(P4 a a1 a2)→P
                           →(ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)→P
BODY =
        assume A0: Set
        assume A1: Set
        assume A2: Set
        assume P0: A0→A1→A2→Prop
        assume P1: A0→A1→A2→Prop
        assume P2: A0→A1→A2→Prop
        assume P3: A0→A1→A2→Prop
        assume P4: A0→A1→A2→Prop
        assume P: Prop
        suppose H: ∀a:A0.∀a1:A1.∀a2:A2.(P0 a a1 a2)→(P1 a a1 a2)→(P2 a a1 a2)→(P3 a a1 a2)→(P4 a a1 a2)→P
        suppose H1: ex5_3 A0 A1 A2 P0 P1 P2 P3 P4
          by cases on H1 we prove P
             case ex5_3_intro a:A0 a1:A1 a2:A2 H2:P0 a a1 a2 H3:P1 a a1 a2 H4:P2 a a1 a2 H5:P3 a a1 a2 H6:P4 a a1 a2 ⇒
                the thesis becomes P
                by (H . . . H2 H3 H4 H5 H6)
P
          we proved P
       we proved 
          ∀A0:Set
            .∀A1:Set
              .∀A2:Set
                .∀P0:A0→A1→A2→Prop
                  .∀P1:A0→A1→A2→Prop
                    .∀P2:A0→A1→A2→Prop
                      .∀P3:A0→A1→A2→Prop
                        .∀P4:A0→A1→A2→Prop
                          .∀P:Prop
                            .∀a:A0.∀a1:A1.∀a2:A2.(P0 a a1 a2)→(P1 a a1 a2)→(P2 a a1 a2)→(P3 a a1 a2)→(P4 a a1 a2)→P
                              →(ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)→P