DEFINITION and4_ind()
TYPE =
∀P0:Prop
.∀P1:Prop.∀P2:Prop.∀P3:Prop.∀P:Prop.(P0→P1→P2→P3→P)→(and4 P0 P1 P2 P3)→P
BODY =
assume P0: Prop
assume P1: Prop
assume P2: Prop
assume P3: Prop
assume P: Prop
suppose H: P0→P1→P2→P3→P
suppose H1: and4 P0 P1 P2 P3
by cases on H1 we prove P
case and4_intro H2:P0 H3:P1 H4:P2 H5:P3 ⇒
the thesis becomes P
by (H H2 H3 H4 H5)
P
we proved P
we proved
∀P0:Prop
.∀P1:Prop.∀P2:Prop.∀P3:Prop.∀P:Prop.(P0→P1→P2→P3→P)→(and4 P0 P1 P2 P3)→P