mb automata 1 Sections GenAutomata Doc

Def ts_fvar(x) == inr(inr(inr(inl(x))))

is mentioned by

Def l == tree_leaf(ts_fvar(l))[tfvar]

Try larger context: GenAutomata

mb automata 1 Sections GenAutomata Doc