r:rel(). rel_primed_vars((r)') = rel_vars(r)t:Term. term_primed_vars((t)') ~ term_vars(t)| Theorem | Name |
|
Thm* r:rel(). rel_primed_vars((r)') = rel_vars(r) | [rel_vars_addprime] |
| cites | |
|
Thm* t:Term. term_primed_vars((t)') ~ term_vars(t) | [term_vars_addprime] |