as:(Label
T) List, d:T, x:Label.
(x 
1of(unzip(as))) 
( < x,apply_alist(as;x;d) > as)as:(LabelT) List, p:(LabelT), l:Label, d:T.
apply_alist([p / as];l;d) ~ if 1of(p) =
l
2of(p) else apply_alist(as;l;d) fi| Theorem | Name |
|
Thm* as:(LabelT) List, d:T, x:Label.
(x 1of(unzip(as))) ( < x,apply_alist(as;x;d) > as) | [apply_alist_member] |
| cites | |
|
Thm* as:(LabelT) List, p:(LabelT), l:Label, d:T.
apply_alist([p / as];l;d) ~ if 1of(p) = l 2of(p) else apply_alist(as;l;d) fi | [apply_alist_cons] |