DEFINITION ex6_6_ind()
TYPE =
∀A0:Set
.∀A1:Set
.∀A2:Set
.∀A3:Set
.∀A4:Set
.∀A5:Set
.∀P0:A0→A1→A2→A3→A4→A5→Prop
.∀P1:A0→A1→A2→A3→A4→A5→Prop
.∀P2:A0→A1→A2→A3→A4→A5→Prop
.∀P3:A0→A1→A2→A3→A4→A5→Prop
.∀P4:A0→A1→A2→A3→A4→A5→Prop
.∀P5:A0→A1→A2→A3→A4→A5→Prop
.∀P:Prop
.∀a:A0
.∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.∀a5:A5.(P0 a a1 a2 a3 a4 a5)→(P1 a a1 a2 a3 a4 a5)→(P2 a a1 a2 a3 a4 a5)→(P3 a a1 a2 a3 a4 a5)→(P4 a a1 a2 a3 a4 a5)→(P5 a a1 a2 a3 a4 a5)→P
→(ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5)→P
BODY =
Show proof