DEFINITION or3_ind() TYPE = ∀P0:Prop .∀P1:Prop.∀P2:Prop.∀P:Prop.(P0→P)→(P1→P)→(P2→P)→(or3 P0 P1 P2)→P BODY =Show proof