At: apply alist cons
T:Type, as:(Label
T) 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
By:
UnivCD
THEN
RW (AddrC [1] (UnfoldC `apply_alist`)) 0
THEN
Unfold `find` 0
THEN
Reduce 0
THEN
SplitOnConclITE
THEN
Reduce 0
THEN
Try ((Fold `find` 0) THEN (Fold `apply_alist` 0))
Generated subgoals:None
About:
