INDUCTIVE DEFINITION and3 () [ :Prop, :Prop, :Prop ]
OF ARITY Prop
BUILT FROM:
     and3_intro: P0→P1→P2→(and3 P0 P1 P2)