is mentioned by

Thm* (Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr))	[Tarski]
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. closed(t) Prop	[term_closed_wf]
Thm* t,x:Term. (t reps x) Prop	[repst_wf]
Thm* t,x:Term. (t reps x Term) Prop	[reps_wf2]
Thm* t:(u Term), x:u. (t reps x u) Prop	[reps_wf]

In prior sections: core