INDUCTIVE DEFINITION and4 () [ :Prop, :Prop, :Prop, :Prop ]
OF ARITY Prop
BUILT FROM:
     and4_intro: P0→P1→P2→P3→(and4 P0 P1 P2 P3)