DEFINITION ex4_ind()
TYPE =
∀A0:Set
.∀P0:A0→Prop
.∀P1:A0→Prop
.∀P2:A0→Prop
.∀P3:A0→Prop
.∀P:Prop
.(∀a:A0.(P0 a)→(P1 a)→(P2 a)→(P3 a)→P)→(ex4 A0 P0 P1 P2 P3)→P
BODY =
assume A0: Set
assume P0: A0→Prop
assume P1: A0→Prop
assume P2: A0→Prop
assume P3: A0→Prop
assume P: Prop
suppose H: ∀a:A0.(P0 a)→(P1 a)→(P2 a)→(P3 a)→P
suppose H1: ex4 A0 P0 P1 P2 P3
by cases on H1 we prove P
case ex4_intro a:A0 H2:P0 a H3:P1 a H4:P2 a H5:P3 a ⇒
the thesis becomes P
by (H . H2 H3 H4 H5)
P
we proved P
we proved
∀A0:Set
.∀P0:A0→Prop
.∀P1:A0→Prop
.∀P2:A0→Prop
.∀P3:A0→Prop
.∀P:Prop
.(∀a:A0.(P0 a)→(P1 a)→(P2 a)→(P3 a)→P)→(ex4 A0 P0 P1 P2 P3)→P