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* {T=} {T}	[discrete_equality_inc_equivalence]

In prior sections: discrete jlc