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] |