r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) 
tc((r)';ds;da;de)t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)| Theorem | Name |
|
Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) tc((r)';ds;da;de) | [tc_addprime] |
| cites | |
|
Thm* t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t) | [term_types_addprime] |