is mentioned by

Thm* Discrete{T} (f:{T=}. True)

[discrete_implies_discrete_equality]

In prior sections: core bool 1