t:Term. Q(q(t)) reps q(t)t:Term. t IN Term 
Q(t) IN Termx:Term. q(x) IN Termt:Term. ref(q(t)) = t| Theorem | Name |
| Thm* t:Term. Q(q(t)) reps q(t) | [qup_up_repst] |
| cites | |
| Thm* t:Term. t IN Term Q(t) IN Term | [qup_termin] |
| Thm* x:Term. q(x) IN Term | [up_termin] |
| Thm* t:Term. ref(q(t)) = t | [down_up] |