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 =
Show proof