DEFINITION ex_2_ind()
TYPE =
       ∀A0:Set.∀A1:Set.∀P0:A0→A1→Prop.∀P:Prop.(∀a:A0.∀a1:A1.(P0 a a1)→P)→(ex_2 A0 A1 P0)→P
BODY =
        assume A0: Set
        assume A1: Set
        assume P0: A0→A1→Prop
        assume P: Prop
        suppose H: ∀a:A0.∀a1:A1.(P0 a a1)→P
        suppose H1: ex_2 A0 A1 P0
          by cases on H1 we prove P
             case ex_2_intro a:A0 a1:A1 H2:P0 a a1 ⇒
                the thesis becomes P
                by (H . . H2)
P
          we proved P
       we proved ∀A0:Set.∀A1:Set.∀P0:A0→A1→Prop.∀P:Prop.(∀a:A0.∀a1:A1.(P0 a a1)→P)→(ex_2 A0 A1 P0)→P