DEFINITION ex2_ind()
TYPE =
       ∀A:Set
         .∀P:A→Prop
           .∀Q:A→Prop
             .∀P:Prop.(∀a:A.(P a)→(Q a)→P)→(ex2 A P Q)→P
BODY =
        assume A: Set
        assume P: A→Prop
        assume Q: A→Prop
        assume P: Prop
        suppose H: ∀a:A.(P a)→(Q a)→P
        suppose H1: ex2 A P Q
          by cases on H1 we prove P
             case ex_intro2 a:A H2:P a H3:Q a ⇒
                the thesis becomes P
                by (H . H2 H3)
P
          we proved P
       we proved 
          ∀A:Set
            .∀P:A→Prop
              .∀Q:A→Prop
                .∀P:Prop.(∀a:A.(P a)→(Q a)→P)→(ex2 A P Q)→P