r:rel(). rel_free_vars((r)') = rel_free_vars(r)t:Term. term_free_vars((t)') ~ term_free_vars(t)| Theorem | Name | ||
| Thm* r:rel(). rel_free_vars((r)') = rel_free_vars(r) | [rel_free_vars_addprime] | ||
| cites | |||
| Thm* t:Term. term_free_vars((t)') ~ term_free_vars(t) | [term_free_vars_addprime] |