DEFINITION ex4_ind()
TYPE =
       ∀A0:Set
         .∀P0:A0→Prop
           .∀P1:A0→Prop
             .∀P2:A0→Prop
               .∀P3:A0→Prop
                 .∀P:Prop
                   .(∀a:A0.(P0 a)→(P1 a)→(P2 a)→(P3 a)→P)→(ex4 A0 P0 P1 P2 P3)→P
BODY =
Show proof