(
Tr:(Term
Prop), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr))
t,e:Term. SUBX(NOT(t); e) = NOT(SUBX(t; e))t:Term. s(t) 
= SUBX(t; s(t))
(A 
B & C) (A C) B) (B C) (A C) P) False| Rank | Theorem | Name |
| 5 | Thm* (Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr)) | [Tarski] |
| cites | ||
| 0 | Thm* t,e:Term. SUBX(NOT(t); e) = NOT(SUBX(t; e)) | [qnot_subx] |
| 4 | Thm* t:Term. s(t) = SUBX(t; s(t)) | [s_reps] |
| 0 | Thm* B (A B & C) (A C) | [prop_and_iff] |
| 0 | Thm* (A B) (B C) (A C) | [prop_iff_trans] |
| 0 | Thm* (P P) False | [prop_iff_contra] |