DEFINITION and5_rect()
TYPE =
ΠP0:Prop
.ΠP1:Prop
.ΠP2:Prop
.ΠP3:Prop
.ΠP4:Prop
.ΠP:(Type:48918:cic:/matita/LAMBDA-TYPES/Base-1/types/defs/and5_rect.con)
.(P0→P1→P2→P3→P4→P)→(and5 P0 P1 P2 P3 P4)→P
BODY =
λP0:Prop
.λP1:Prop
.λP2:Prop
.λP3:Prop
.λP4:Prop
.λP:(Type:48918:cic:/matita/LAMBDA-TYPES/Base-1/types/defs/and5_rect.con)
.λf:P0→P1→P2→P3→P4→P
.λH:and5 P0 P1 P2 P3 P4.<λH1:and5 P0 P1 P2 P3 P4.P> CASE H OF and5_intro H1 H2 H3 H4 H5⇒f H1 H2 H3 H4 H5