is mentioned by

Thm* eq:{T=}, x,y:T. eq(x,y) eq(y,x)	[discrete_equality_symmetric]
Thm* eq:{T=}. (x,y:T. eq(x,y) x = y) & eq TT	[discrete_equality_properties]
Thm* Discrete{T} (f:(TT). x,y:T. f(x,y) x = y)	[discrete_implies_bool_equality]
Def {T=} == {eq:(TT)| x,y:T. (eq(x,y)) x = y }	[discrete_equality]

In prior sections: core well fnd int 1 bool 1 bool 2 jlc