is mentioned by

Def d o f(x) == y:Label. if x = f(y) d(y) else Top fi	[rename_decl]
Def x:y(a) == if a = x y else Top fi	[dbase]

In prior sections: mb basic

Try larger context: GenAutomata