A:ioa{i:l}(), a:Label, P:Fmla. wp2(A;a;(P)') = wp(A;a;P)r:rel(), as:(Label
Term) List. 1of(unzip(as)) = rel_vars(r) 
rel_subst2(as;(r)') = rel_subst(as;r)| Rank | Theorem | Name | ||
| 5 | Thm* A:ioa{i:l}(), a:Label, P:Fmla. wp2(A;a;(P)') = wp(A;a;P) | [wp2_addprime] | ||
| cites | ||||
| 4 | Thm* r:rel(), as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) rel_subst2(as;(r)') = rel_subst(as;r) | [rel_subst2_addprime] |