t:Term. UP(
t) 
= tt:Term. t 
Term 
UP(t) Termx:Term. x Termt:Term. t = t| Theorem | Name |
| Thm* t:Term. UP(t) = t | [qup_up_repst] |
| cites | |
| Thm* t:Term. t Term UP(t) Term | [qup_termin] |
| Thm* x:Term. x Term | [up_termin] |
| Thm* t:Term. t = t | [down_up] |