r:rel(), rho,ds,da1,da2,de,s,e,a1,a2,tr:Top.
closed_rel(r) 
([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr)t:Term, e,s,a1,a2,tr:Top.
closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)| Theorem | Name |
|
Thm* r:rel(), rho,ds,da1,da2,de,s,e,a1,a2,tr:Top.
closed_rel(r) ([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr) | [closed_rel_mng_sq] |
| cites | |
|
Thm* t:Term, e,s,a1,a2,tr:Top.
closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr) | [closed_term_mng] |