+inductive or5 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop) (P4: Prop): Prop
+\def
+| or5_intro0: P0 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro1: P1 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro2: P2 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro3: P3 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro4: P4 \to (or5 P0 P1 P2 P3 P4).
+