At: apply alist member 2 1 1 1
1. T: Type
2. as: (Label
T) List
3. u: Label
T
4. v: (Label
T) List
5.
d:T, x:Label. (x
map(
p.1of(p);v)) 
( < x,apply_alist(v;x;d) >
v)
6. d: T
7. x: Label
8. x = 1of(u)
(x
map(
p.1of(p);v))
9. apply_alist([u / v];x;d) ~ if 1of(u) =
x
2of(u) else apply_alist(v;x;d) fi
10. 1of(u) = x
Pattern
< x,2of(u) > = u
( < x,2of(u) >
v)
By: Sel 1 (Analyze 0)
Generated subgoal:1 | < x,2of(u) > = u |
About: