INDUCTIVE DEFINITION or4 () [ :Prop, :Prop, :Prop, :Prop ]
OF ARITY Prop
BUILT FROM:
     or4_intro0: P0→(or4 P0 P1 P2 P3)
   | or4_intro1: P1→(or4 P0 P1 P2 P3)
   | or4_intro2: P2→(or4 P0 P1 P2 P3)
   | or4_intro3: P3→(or4 P0 P1 P2 P3)