is mentioned by

Def Discrete{T} == x,y:T. Dec(x = y)

[discrete]

In prior sections: core int 1 bool 1