is mentioned by

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]