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