DEFINITION ex2_3_ind()
TYPE =
       ∀A0:Set
         .∀A1:Set
           .∀A2:Set
             .∀P0:A0→A1→A2→Prop
               .∀P1:A0→A1→A2→Prop
                 .∀P:Prop.(∀a:A0.∀a1:A1.∀a2:A2.(P0 a a1 a2)→(P1 a a1 a2)→P)→(ex2_3 A0 A1 A2 P0 P1)→P
BODY =
Show proof