DEFINITION ex3_4_ind()
TYPE =
∀A0:Set
.∀A1:Set
.∀A2:Set
.∀A3:Set
.∀P0:A0→A1→A2→A3→Prop
.∀P1:A0→A1→A2→A3→Prop
.∀P2:A0→A1→A2→A3→Prop
.∀P:Prop.(∀a:A0.∀a1:A1.∀a2:A2.∀a3:A3.(P0 a a1 a2 a3)→(P1 a a1 a2 a3)→(P2 a a1 a2 a3)→P)→(ex3_4 A0 A1 A2 A3 P0 P1 P2)→P
BODY =
assume A0: Set
assume A1: Set
assume A2: Set
assume A3: Set
assume P0: A0→A1→A2→A3→Prop
assume P1: A0→A1→A2→A3→Prop
assume P2: A0→A1→A2→A3→Prop
assume P: Prop
suppose H: ∀a:A0.∀a1:A1.∀a2:A2.∀a3:A3.(P0 a a1 a2 a3)→(P1 a a1 a2 a3)→(P2 a a1 a2 a3)→P
suppose H1: ex3_4 A0 A1 A2 A3 P0 P1 P2
by cases on H1 we prove P
case ex3_4_intro a:A0 a1:A1 a2:A2 a3:A3 H2:P0 a a1 a2 a3 H3:P1 a a1 a2 a3 H4:P2 a a1 a2 a3 ⇒
the thesis becomes P
by (H . . . . H2 H3 H4)
P
we proved P
we proved
∀A0:Set
.∀A1:Set
.∀A2:Set
.∀A3:Set
.∀P0:A0→A1→A2→A3→Prop
.∀P1:A0→A1→A2→A3→Prop
.∀P2:A0→A1→A2→A3→Prop
.∀P:Prop.(∀a:A0.∀a1:A1.∀a2:A2.∀a3:A3.(P0 a a1 a2 a3)→(P1 a a1 a2 a3)→(P2 a a1 a2 a3)→P)→(ex3_4 A0 A1 A2 A3 P0 P1 P2)→P