r:rel(), rho,ds,da,de,e,s,a,tr,tr':Top.
rel_mentions_trace(r) 
([[r]] rho ds da de e s a tr' ~ [[r]] rho ds da de e s a tr)u:Term, e,s,a,tr,tr':Top.
mentions_trace(u) ([[u]] e s a tr' ~ [[u]] e s a tr)| Theorem | Name |
|
Thm* r:rel(), rho,ds,da,de,e,s,a,tr,tr':Top.
rel_mentions_trace(r) ([[r]] rho ds da de e s a tr' ~ [[r]] rho ds da de e s a tr) | [rel_mng_static] |
| cites | |
|
Thm* u:Term, e,s,a,tr,tr':Top.
mentions_trace(u) ([[u]] e s a tr' ~ [[u]] e s a tr) | [term_mng_static] |