is mentioned by

Thm* x:Label, ls:Label List. x ls (x ls)

[assert_lbls_member]

In prior sections: mb list 1

Try larger context: GenAutomata