as:(Label
T) List, d1,d2:T, x:Label.
(x 
1of(unzip(as))) 
apply_alist(as;x;d1) = apply_alist(as;x;d2)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, d1,d2:T, x:Label.
(x 1of(unzip(as))) apply_alist(as;x;d1) = apply_alist(as;x;d2) | [apply_alist_member2] |
| 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] |