INDUCTIVE DEFINITION ex5_3 () [ A0:Set, A1:Set, A2:Set, :A0A1A2Prop, :A0A1A2Prop, :A0A1A2Prop, :A0A1A2Prop, :A0A1A2Prop ]
OF ARITY Prop
BUILT FROM:
     ex5_3_intro: x0:A0.x1:A1.x2:A2.(P0 x0 x1 x2)(P1 x0 x1 x2)(P2 x0 x1 x2)(P3 x0 x1 x2)(P4 x0 x1 x2)(ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)