DEFINITION ex4_5_ind()
TYPE =
       ∀A0:Set
         .∀A1:Set
           .∀A2:Set
             .∀A3:Set
               .∀A4:Set
                 .∀P0:A0→A1→A2→A3→A4→Prop
                   .∀P1:A0→A1→A2→A3→A4→Prop
                     .∀P2:A0→A1→A2→A3→A4→Prop
                       .∀P3:A0→A1→A2→A3→A4→Prop
                         .∀P:Prop
                           .(∀a:A0.∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.(P0 a a1 a2 a3 a4)→(P1 a a1 a2 a3 a4)→(P2 a a1 a2 a3 a4)→(P3 a a1 a2 a3 a4)→P)→(ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3)→P
BODY =
Show proof