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