INDUCTIVE DEFINITION ex6_7 () [ A0:Set, A1:Set, A2:Set, A3:Set, A4:Set, A5:Set, A6:Set, :A0→A1→A2→A3→A4→A5→A6→Prop, :A0→A1→A2→A3→A4→A5→A6→Prop, :A0→A1→A2→A3→A4→A5→A6→Prop, :A0→A1→A2→A3→A4→A5→A6→Prop, :A0→A1→A2→A3→A4→A5→A6→Prop, :A0→A1→A2→A3→A4→A5→A6→Prop ]
OF ARITY Prop
BUILT FROM:
     ex6_7_intro: ∀x0:A0.∀x1:A1.∀x2:A2.∀x3:A3.∀x4:A4.∀x5:A5.∀x6:A6.(P0 x0 x1 x2 x3 x4 x5 x6)→(P1 x0 x1 x2 x3 x4 x5 x6)→(P2 x0 x1 x2 x3 x4 x5 x6)→(P3 x0 x1 x2 x3 x4 x5 x6)→(P4 x0 x1 x2 x3 x4 x5 x6)→(P5 x0 x1 x2 x3 x4 x5 x6)→(ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5)