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