is mentioned by

Thm* Discrete{T} (f:{T=}. True)	[discrete_implies_discrete_equality]
Thm* Discrete{T} (f:(TT). x,y:T. f(x,y) x = y)	[discrete_implies_bool_equality]

In prior sections: core