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