DEFINITION ex3_ind() TYPE = ∀A0:Set .∀P0:A0→Prop .∀P1:A0→Prop .∀P2:A0→Prop .∀P:Prop.(∀a:A0.(P0 a)→(P1 a)→(P2 a)→P)→(ex3 A0 P0 P1 P2)→P BODY =Show proof