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