INDUCTIVE DEFINITION ex4 () [ A0:Set, :A0→Prop, :A0→Prop, :A0→Prop, :A0→Prop ]
OF ARITY Prop
BUILT FROM:
     ex4_intro: ∀x0:A0.(P0 x0)→(P1 x0)→(P2 x0)→(P3 x0)→(ex4 A0 P0 P1 P2 P3)