is mentioned by

Thm* eq:{T}, f:{T=}, x,y:T. eq(x,y) f(x,y)	[not_equivalence_implies_not_discrete_eq]
Thm* eq:{T=}, f:{T}, x,y:T. eq(x,y) f(x,y)	[equivalence_weakening_lemma]
Thm* EQ:{T=}. EQ {T}	[discrete_equality_is_equivalence]
Thm* eq:{T}, u:T. eq(u,u)	[equivalence_reflexive]
Thm* eq:{T}. eq TT	[equivalence_bool_function]
Thm* eq:{T}, x,y:T. eq(x,y) eq(y,x)	[equivalence_symmetric]
Thm* f:{T}. (x,y,z:T. f(x,y) f(y,z) f(x,z)) & (x,y:T. f(x,y) f(y,x)) & (x:T. f(x,x)) & f TT	[equivalence_properties]
Thm* eq:{T}. eq TT	[equivalence_type]
Thm* {T=} {T}	[discrete_equality_inc_equivalence]
Thm* {T} (TT)	[equivalence_inc]