DEFINITION or5_ind()
TYPE =
       ∀P0:Prop
         .∀P1:Prop
           .∀P2:Prop
             .∀P3:Prop
               .∀P4:Prop
                 .∀P:Prop
                   .P0→P
                     →(P1→P)→(P2→P)→(P3→P)→(P4→P)→(or5 P0 P1 P2 P3 P4)→P
BODY =
Show proof