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: bool 1 mb nat int 2 list 1 prog 1 num thy 1 mb list 1

Try larger context: GenAutomata