DEFINITION and5_rec() TYPE = ΠP0:Prop .ΠP1:Prop .ΠP2:Prop .ΠP3:Prop .ΠP4:Prop .ΠP:Set.(P0→P1→P2→P3→P4→P)→(and5 P0 P1 P2 P3 P4)→P BODY =Show proof