DEFINITION ex6_6_ind()
TYPE =
       ∀A0:Set
         .∀A1:Set
           .∀A2:Set
             .∀A3:Set
               .∀A4:Set
                 .∀A5:Set
                   .∀P0:A0→A1→A2→A3→A4→A5→Prop
                     .∀P1:A0→A1→A2→A3→A4→A5→Prop
                       .∀P2:A0→A1→A2→A3→A4→A5→Prop
                         .∀P3:A0→A1→A2→A3→A4→A5→Prop
                           .∀P4:A0→A1→A2→A3→A4→A5→Prop
                             .∀P5:A0→A1→A2→A3→A4→A5→Prop
                               .∀P:Prop
                                 .∀a:A0
                                     .∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.∀a5:A5.(P0 a a1 a2 a3 a4 a5)→(P1 a a1 a2 a3 a4 a5)→(P2 a a1 a2 a3 a4 a5)→(P3 a a1 a2 a3 a4 a5)→(P4 a a1 a2 a3 a4 a5)→(P5 a a1 a2 a3 a4 a5)→P
                                   →(ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5)→P
BODY =
        assume A0: Set
        assume A1: Set
        assume A2: Set
        assume A3: Set
        assume A4: Set
        assume A5: Set
        assume P0: A0→A1→A2→A3→A4→A5→Prop
        assume P1: A0→A1→A2→A3→A4→A5→Prop
        assume P2: A0→A1→A2→A3→A4→A5→Prop
        assume P3: A0→A1→A2→A3→A4→A5→Prop
        assume P4: A0→A1→A2→A3→A4→A5→Prop
        assume P5: A0→A1→A2→A3→A4→A5→Prop
        assume P: Prop
        suppose H: 
           ∀a:A0
             .∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.∀a5:A5.(P0 a a1 a2 a3 a4 a5)→(P1 a a1 a2 a3 a4 a5)→(P2 a a1 a2 a3 a4 a5)→(P3 a a1 a2 a3 a4 a5)→(P4 a a1 a2 a3 a4 a5)→(P5 a a1 a2 a3 a4 a5)→P
        suppose H1: ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5
          by cases on H1 we prove P
             case ex6_6_intro a:A0 a1:A1 a2:A2 a3:A3 a4:A4 a5:A5 H2:P0 a a1 a2 a3 a4 a5 H3:P1 a a1 a2 a3 a4 a5 H4:P2 a a1 a2 a3 a4 a5 H5:P3 a a1 a2 a3 a4 a5 H6:P4 a a1 a2 a3 a4 a5 H7:P5 a a1 a2 a3 a4 a5 ⇒
                the thesis becomes P
                by (H . . . . . . H2 H3 H4 H5 H6 H7)
P
          we proved P
       we proved 
          ∀A0:Set
            .∀A1:Set
              .∀A2:Set
                .∀A3:Set
                  .∀A4:Set
                    .∀A5:Set
                      .∀P0:A0→A1→A2→A3→A4→A5→Prop
                        .∀P1:A0→A1→A2→A3→A4→A5→Prop
                          .∀P2:A0→A1→A2→A3→A4→A5→Prop
                            .∀P3:A0→A1→A2→A3→A4→A5→Prop
                              .∀P4:A0→A1→A2→A3→A4→A5→Prop
                                .∀P5:A0→A1→A2→A3→A4→A5→Prop
                                  .∀P:Prop
                                    .∀a:A0
                                        .∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.∀a5:A5.(P0 a a1 a2 a3 a4 a5)→(P1 a a1 a2 a3 a4 a5)→(P2 a a1 a2 a3 a4 a5)→(P3 a a1 a2 a3 a4 a5)→(P4 a a1 a2 a3 a4 a5)→(P5 a a1 a2 a3 a4 a5)→P
                                      →(ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5)→P