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