DEFINITION or4_ind() TYPE = ∀P0:Prop .∀P1:Prop .∀P2:Prop .∀P3:Prop .∀P:Prop .(P0→P)→(P1→P)→(P2→P)→(P3→P)→(or4 P0 P1 P2 P3)→P BODY =Show proof