is mentioned by

Thm* f1,f2:{T=}. f1 = f2 TT	[discrete_equality_unique]
Thm* eq:{T=}. (x,y:T. eq(x,y) x = y) & eq TT	[discrete_equality_properties]
Thm* {T=} (TT)	[discrete_equality_inc]
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: bool 1 bool 2 jlc