INDUCTIVE DEFINITION or5 () [ :Prop, :Prop, :Prop, :Prop, :Prop ]
OF ARITY Prop
BUILT FROM:
     or5_intro0: P0→(or5 P0 P1 P2 P3 P4)
   | or5_intro1: P1→(or5 P0 P1 P2 P3 P4)
   | or5_intro2: P2→(or5 P0 P1 P2 P3 P4)
   | or5_intro3: P3→(or5 P0 P1 P2 P3 P4)
   | or5_intro4: P4→(or5 P0 P1 P2 P3 P4)