t,r,t',r':Term. t reps t' & r reps r' 
SUBX(t; r) reps t'/r't,r:Term. t IN Term & r IN Term SUBX(t; r) IN Term| Theorem | Name |
| Thm* t,r,t',r':Term. t reps t' & r reps r' SUBX(t; r) reps t'/r' | [qsubx_repst] |
| cites | |
| Thm* t,r:Term. t IN Term & r IN Term SUBX(t; r) IN Term | [qsubx_termin] |