as:(Label
T) List, d:T, x:Label.
(x 
1of(unzip(as))) 
apply_alist(as;x;d) = dd:Top, l:Label. apply_alist(nil;l;d) ~ das:(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))) apply_alist(as;x;d) = d | [apply_alist_non_member] |
| cites | |
|
Thm* d:Top, l:Label. apply_alist(nil;l;d) ~ d | [apply_alist_nil] |
|
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] |