is mentioned by

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(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]

In prior sections: core bool 1