DEFINITION ex6_7_ind()
TYPE =
∀A0:Set
.∀A1:Set
.∀A2:Set
.∀A3:Set
.∀A4:Set
.∀A5:Set
.∀A6:Set
.∀P0:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P1:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P2:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P3:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P4:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P5:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P:Prop
.∀a:A0
.∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.∀a5:A5.∀a6:A6.(P0 a a1 a2 a3 a4 a5 a6)→(P1 a a1 a2 a3 a4 a5 a6)→(P2 a a1 a2 a3 a4 a5 a6)→(P3 a a1 a2 a3 a4 a5 a6)→(P4 a a1 a2 a3 a4 a5 a6)→(P5 a a1 a2 a3 a4 a5 a6)→P
→(ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5)→P
BODY =
assume A0: Set
assume A1: Set
assume A2: Set
assume A3: Set
assume A4: Set
assume A5: Set
assume A6: Set
assume P0: A0→A1→A2→A3→A4→A5→A6→Prop
assume P1: A0→A1→A2→A3→A4→A5→A6→Prop
assume P2: A0→A1→A2→A3→A4→A5→A6→Prop
assume P3: A0→A1→A2→A3→A4→A5→A6→Prop
assume P4: A0→A1→A2→A3→A4→A5→A6→Prop
assume P5: A0→A1→A2→A3→A4→A5→A6→Prop
assume P: Prop
suppose H:
∀a:A0
.∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.∀a5:A5.∀a6:A6.(P0 a a1 a2 a3 a4 a5 a6)→(P1 a a1 a2 a3 a4 a5 a6)→(P2 a a1 a2 a3 a4 a5 a6)→(P3 a a1 a2 a3 a4 a5 a6)→(P4 a a1 a2 a3 a4 a5 a6)→(P5 a a1 a2 a3 a4 a5 a6)→P
suppose H1: ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5
by cases on H1 we prove P
case ex6_7_intro a:A0 a1:A1 a2:A2 a3:A3 a4:A4 a5:A5 a6:A6 H2:P0 a a1 a2 a3 a4 a5 a6 H3:P1 a a1 a2 a3 a4 a5 a6 H4:P2 a a1 a2 a3 a4 a5 a6 H5:P3 a a1 a2 a3 a4 a5 a6 H6:P4 a a1 a2 a3 a4 a5 a6 H7:P5 a a1 a2 a3 a4 a5 a6 ⇒
the thesis becomes P
by (H . . . . . . . H2 H3 H4 H5 H6 H7)
P
we proved P
we proved
∀A0:Set
.∀A1:Set
.∀A2:Set
.∀A3:Set
.∀A4:Set
.∀A5:Set
.∀A6:Set
.∀P0:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P1:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P2:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P3:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P4:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P5:A0→A1→A2→A3→A4→A5→A6→Prop
.∀P:Prop
.∀a:A0
.∀a1:A1.∀a2:A2.∀a3:A3.∀a4:A4.∀a5:A5.∀a6:A6.(P0 a a1 a2 a3 a4 a5 a6)→(P1 a a1 a2 a3 a4 a5 a6)→(P2 a a1 a2 a3 a4 a5 a6)→(P3 a a1 a2 a3 a4 a5 a6)→(P4 a a1 a2 a3 a4 a5 a6)→(P5 a a1 a2 a3 a4 a5 a6)→P
→(ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5)→P