r:rel(), x:Label. (x 
rel_primed_vars(r)) 
(x rel_vars(r))x:Label, u:Term.
(x term_primed_vars(u)) (x term_vars(u))| Theorem | Name |
|
Thm* r:rel(), x:Label. (x rel_primed_vars(r)) (x rel_vars(r)) | [rel_primed_vars_rel_vars] |
| cites | |
|
Thm* x:Label, u:Term.
(x term_primed_vars(u)) (x term_vars(u)) | [term_primed_vars_term_vars] |