is mentioned by

Def P Q == P + Q

[pred_and]

In prior sections: mb collection

Try larger context: GenAutomata