t:Term. s(t) 
= SUBX(t; SUBX(f(t); 
f(t)))t:Term. s(t) = SUBX(t; SUBX(f(t); UP(f(t))))t,r,t',r':Term. t = t' & r = r' 
SUBX(t; r) = SUBX(t'; r')t:Term. t = tt:Term. UP(t) = t| Rank | Theorem | Name |
| 3 | Thm* t:Term. s(t) = SUBX(t; SUBX(f(t); f(t))) | [s2] |
| cites | ||
| 2 | Thm* t:Term. s(t) = SUBX(t; SUBX(f(t); UP(f(t)))) | [s1] |
| 1 | Thm* t,r,t',r':Term. t = t' & r = r' SUBX(t; r) = SUBX(t'; r') | [qsubx_repst] |
| 2 | Thm* t:Term. t = t | [up_repst] |
| 1 | Thm* t:Term. UP(t) = t | [qup_up_repst] |