DEFINITION and4_rect()
TYPE =
ΠP0:Prop
.ΠP1:Prop
.ΠP2:Prop
.ΠP3:Prop
.ΠP:(Type:47727:cic:/matita/LAMBDA-TYPES/Base-1/types/defs/and4_rect.con)
.(P0→P1→P2→P3→P)→(and4 P0 P1 P2 P3)→P
BODY =
Show proof