is mentioned by

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* (P Q) (Dec(P) Dec(Q))	[decidable_functionality_wrt_iff]
Thm* SqStable(P) SqStable(Q) SqStable(P Q) SqStable(P) SqStable(Q)	[sq_stable_functionality_wrt_or]

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