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 =
Show proof