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]
Thm* Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr) Prop	[RepsTruth_wf]
Thm* P:(TermProp), qP:Term, L:(TermProp). ReflectsProp(P; qP; L) Prop	[ReflectsProp_wf]
Thm* Tr,L:(TermProp). RespectsNot(Tr; L) Prop	[RespectsNot_wf]
Thm* t:Term. s(t) = SUBX(t; s(t))	[s_reps]
Thm* t:Term. s(t) = SUBX(t; SUBX(f(t); f(t)))	[s2]
Thm* t:Term. s(t) = SUBX(t; SUBX(f(t); UP(f(t))))	[s1]
Thm* t:Term. s(t) Term	[s_wf]
Thm* t:Term. f(t) Term	[f_wf]
Thm* t,e:Term. SUBX(NOT(t); e) = NOT(SUBX(t; e))	[qnot_subx]
Thm* t,r,t',r':Term. t = t' & r = r' SUBX(t; r) = SUBX(t'; r')	[qsubx_repst]
Thm* t,r:Term. SUBX(t; r) Term	[subx_wf]
Thm* t:Term. UP(t) = t	[qup_up_repst]
Thm* t:Term. closed(t)	[up_term_closed]
Thm* t:Term. closed(t) Prop	[term_closed_wf]
Thm* t:Term. t = t	[up_repst]
Thm* t:Term. t = t	[up_reps]
Thm* t,x:Term. (t = x) Prop	[repst_wf]
Thm* t,x:Term. (t = x) Prop	[reps_wf2]
Thm* t:(u Term), x:u. (t = x) Prop	[reps_wf]
Thm* (A Term) Type	[termof_wf]
Def RepsTruth(L; Tr; tr) == (S:Term. (t:Term. S = t) L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr)	[RepsTruth]
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]
Def closed(t) == s,v:Term. t[s/v] = t	[term_closed]

In prior sections: core