DEFINITION ex_ind()
TYPE =
       ∀A:Set.∀P:A→Prop.∀P:Prop.(∀a:A.(P a)→P)→(ex A P)→P
BODY =
        assume A: Set
        assume P: A→Prop
        assume P: Prop
        suppose H: ∀a:A.(P a)→P
        suppose H1: ex A P
          by cases on H1 we prove P
             case ex_intro a:A H2:P a ⇒
                the thesis becomes P
                by (H . H2)
P
          we proved P
       we proved ∀A:Set.∀P:A→Prop.∀P:Prop.(∀a:A.(P a)→P)→(ex A P)→P