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