r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) 
tc(rel_unprime(r);ds;da;de)v:Top, rho:Decl. v 
[[ < > ]] rhot:Term, ds,da,de:Top.
term_types(ds;da;de;unprime(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(rel_unprime(r);ds;da;de) | [tc_unprime] |
| cites | |
|
Thm* v:Top, rho:Decl. v [[ < > ]] rho | [empty_sts_mng] |
|
Thm* t:Term, ds,da,de:Top.
term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t) | [term_types_unprime] |