is mentioned by

Thm* T1:Type{i}, T2:Type{j}. Discrete{T1} Discrete{T2} Discrete{(T1T2)}	[discrete__product]
Thm* T1:Type{i}, T2:Type{j}. Discrete{T1} Discrete{T2} Discrete{(T1+T2)}	[discrete__union]
Thm* eq:{T=}, x,y,z:T. eq(x,y) eq(y,z) eq(x,z)	[discrete_equality_transitive]
Thm* eq:{T=}, x,y:T. eq(x,y) eq(y,x)	[discrete_equality_symmetric]
Thm* eq:{T=}, u:T. eq(u,u)	[discrete_equality_reflexive]
Thm* f1,f2:{T=}. f1 = f2 TT	[discrete_equality_unique]
Thm* Discrete{T} (f:{T=}. True)	[discrete_implies_discrete_equality]
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]
Def Discrete{T} == x,y:T. Dec(x = y)	[discrete]

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