is mentioned by

Thm* P:(TProp). (x:T. Dec(P(x))) (x:T. P(x) P(x))	[not_not_rw]
Thm* P:(TUProp). (x:T, y:U. Dec(P(x,y))) (p:(TU). Dec(p/l,r. P(l,r)))	[decidable__spread]
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]
Thm* t1,t2:T, u1,u2:U. t1 = t2 u1 = u2 < t1,u1 > = < t2,u2 >	[pair_functionality_wrt_equal]
Thm* Dec(P) Dec(Q) ((P Q) (Q P))	[contrapositive]
Thm* Dec(P) Dec(Q) ((P & Q) P Q)	[demorgan2]
Thm* Dec(P) Dec(Q) ((P Q) P & Q)	[demorgan1]
Thm* Dec(P) Dec(Q) ((P Q) P & Q)	[demorgan]
Thm* Dec(nil = nil T List)	[decidable__equal_nil]
Thm* (P Q) (Dec(P) Dec(Q))	[decidable_functionality_wrt_iff]
Thm* Dec(P) Dec(Q) SqStable(P Q)	[sq_stable__or]
Thm* SqStable(P) SqStable(Q) SqStable(P Q) SqStable(P) SqStable(Q)	[sq_stable_functionality_wrt_or]
Thm* P:(TZProp). (x:T, y:Z. Dec(P(x,y))) (f_p:(TZ). x:T, y:Z. P(x,y) f_p(x,y))	[decidable_iff_exists_bool_function_2]
Thm* P:(TProp). (x:T. Dec(P(x))) (f_p:(T). x:T. P(x) f_p(x))	[decidable_iff_exists_bool_function]
Def {T} == {f:(TT)| (x:T. (f(x,x))) & (x,y:T. (f(x,y)) (f(y,x))) & (x,y,z:T. (f(x,y)) (f(y,z)) (f(x,z))) }	[equivalence]

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