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