DEFINITION ex3_2_ind()
TYPE =
       ∀A0:Set
         .∀A1:Set
           .∀P0:A0→A1→Prop
             .∀P1:A0→A1→Prop
               .∀P2:A0→A1→Prop
                 .∀P:Prop.(∀a:A0.∀a1:A1.(P0 a a1)→(P1 a a1)→(P2 a a1)→P)→(ex3_2 A0 A1 P0 P1 P2)→P
BODY =
Show proof