DEFINITION ex3_ind()
TYPE =
       ∀A0:Set
         .∀P0:A0→Prop
           .∀P1:A0→Prop
             .∀P2:A0→Prop
               .∀P:Prop.(∀a:A0.(P0 a)→(P1 a)→(P2 a)→P)→(ex3 A0 P0 P1 P2)→P
BODY =
        assume A0: Set
        assume P0: A0→Prop
        assume P1: A0→Prop
        assume P2: A0→Prop
        assume P: Prop
        suppose H: ∀a:A0.(P0 a)→(P1 a)→(P2 a)→P
        suppose H1: ex3 A0 P0 P1 P2
          by cases on H1 we prove P
             case ex3_intro a:A0 H2:P0 a H3:P1 a H4:P2 a ⇒
                the thesis becomes P
                by (H . H2 H3 H4)
P
          we proved P
       we proved 
          ∀A0:Set
            .∀P0:A0→Prop
              .∀P1:A0→Prop
                .∀P2:A0→Prop
                  .∀P:Prop.(∀a:A0.(P0 a)→(P1 a)→(P2 a)→P)→(ex3 A0 P0 P1 P2)→P