mb automata 2 Sections GenAutomata Doc

Def ab == tree_node( < a, b > )

is mentioned by

Thm* c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1)[member_st_app]
Thm* s1,s2,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2s)[member_st_app1]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc