INDUCTIVE DEFINITION and5 () [ :Prop, :Prop, :Prop, :Prop, :Prop ]
OF ARITY Prop
BUILT FROM:
     and5_intro: P0→P1→P2→P3→P4→(and5 P0 P1 P2 P3 P4)