mb automata 2 Sections GenAutomata Doc

Def c1 c2 == x:T. x c1 x c2

is mentioned by

Thm* a1,a2,b1,b2:Collection(SimpleType). a1 a2 b1 b2 st_app(a1;b1) st_app(a2;b2)[st_app_monotone]
Thm* x:Label, a1,a2:Collection(dec()). a1 a2 dec_lookup(a1;x) dec_lookup(a2;x)[dec_lookup_monotone]

In prior sections: mb collection

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc