r:rel(), rho,ds,da,de,e,s,s',a,tr:Top.
rel_mng_2(rel_unprime(r); rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s a trt:Term, e,s,s',a,tr:Top. [[unprime(t)]] e s s' a tr ~ [[t]] e s a tr| Theorem | Name |
|
Thm* r:rel(), rho,ds,da,de,e,s,s',a,tr:Top.
rel_mng_2(rel_unprime(r); rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s a tr | [rel_mng_2_unprime] |
| cites | |
|
Thm* t:Term, e,s,s',a,tr:Top. [[unprime(t)]] e s s' a tr ~ [[t]] e s a tr | [term_mng2_unprime] |