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