as:(Label
T) List, d:T, x:Label.
(apply_alist(as;x;d) 
2of(unzip(as))) 
apply_alist(as;x;d) = dP:(T
), as:T List, d:T.
((first a as s.t. P(a) else d) as) (first a as s.t. P(a) else d) = d| Theorem | Name |
|
Thm* as:(LabelT) List, d:T, x:Label.
(apply_alist(as;x;d) 2of(unzip(as))) apply_alist(as;x;d) = d | [apply_alist_property] |
| cites | |
|
Thm* P:(T), as:T List, d:T.
((first a as s.t. P(a) else d) as) (first a as s.t. P(a) else d) = d | [find_property] |