is mentioned by

Thm* P:(TProp). (x:T. Dec(P(x))) (x:T. P(x) P(x))	[not_not_rw]
Thm* eq:{T}, f:{T=}, x,y:T. eq(x,y) f(x,y)	[not_equivalence_implies_not_discrete_eq]
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]

In prior sections: core bool 1 bool 2 jlc