Q:Fmla. closed_pred((Q)') 
closed_pred(Q)r:rel(). rel_free_vars((r)') = rel_free_vars(r)| Rank | Theorem | Name |
| 2 |
Thm* Q:Fmla. closed_pred((Q)') closed_pred(Q) | [closed_pred_addprime] |
| cites | ||
| 1 |
Thm* r:rel(). rel_free_vars((r)') = rel_free_vars(r) | [rel_free_vars_addprime] |