is mentioned
In prior sections: sqequal 1 prog 1 mb basic mb label mb automata 1 mb automata 2
Try larger context: GenAutomata
x,y:T. x = y 
{x ~ y}