| or4_intro2: P2 \to (or4 P0 P1 P2 P3)
| or4_intro3: P3 \to (or4 P0 P1 P2 P3).
+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).
+
inductive ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to
Prop): Prop \def
| ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0