DEFINITION ex6_7_ind()
TYPE =
       ∀A0:Set
         .∀A1:Set
           .∀A2:Set
             .∀A3:Set
               .∀A4:Set
                 .∀A5:Set
                   .∀A6:Set
                     .∀P0:A0→A1→A2→A3→A4→A5→A6→Prop
                       .∀P1:A0→A1→A2→A3→A4→A5→A6→Prop
                         .∀P2:A0→A1→A2→A3→A4→A5→A6→Prop
                           .∀P3:A0→A1→A2→A3→A4→A5→A6→Prop
                             .∀P4:A0→A1→A2→A3→A4→A5→A6→Prop
                               .∀P5:A0→A1→A2→A3→A4→A5→A6→Prop
                                 .∀P:Prop
                                   .∀a:A0
                                       .∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.∀a5:A5.∀a6:A6.(P0 a a1 a2 a3 a4 a5 a6)→(P1 a a1 a2 a3 a4 a5 a6)→(P2 a a1 a2 a3 a4 a5 a6)→(P3 a a1 a2 a3 a4 a5 a6)→(P4 a a1 a2 a3 a4 a5 a6)→(P5 a a1 a2 a3 a4 a5 a6)→P
                                     →(ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5)→P
BODY =
Show proof