Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') 
covers_pred(A;Q)x:Label, u:Term.
(x 
term_primed_vars(u)) 
(x term_vars(u))t:Term. term_primed_vars((t)') ~ term_vars(t)| Theorem | Name |
|
Thm* Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') covers_pred(A;Q) | [covers_pred_addprime] |
| cites | |
|
Thm* x:Label, u:Term.
(x term_primed_vars(u)) (x term_vars(u)) | [term_primed_vars_term_vars] |
|
Thm* t:Term. term_primed_vars((t)') ~ term_vars(t) | [term_vars_addprime] |