is mentioned by

Thm* (P P) False	[prop_iff_contra]
Thm* (A B) (B C) (A C)	[prop_iff_trans]
Thm* B (A B & C) (A C)	[prop_and_iff]
Def ReflectsProp(P; qP; Tr) == t,qt:Term. qt = t {Tr(SUBX(qP; qt)) Tr(t)}	[ReflectsProp]
Def RespectsNot(Tr; L) == t:Term. Tr(NOT(t)) L(t) & Tr(t)	[RespectsNot]

In prior sections: core