7. x: Label
8. x = 1of(u)
(x 
map(
p.1of(p);v))
< x,apply_alist([u / v];x;d) > = u ( < x,apply_alist([u / v];x;d) > v)
T) ListTT) List
d:T, x:Label. (x map(p.1of(p);v)) 
( < x,apply_alist(v;x;d) > v) d:T, x:Label. (x [1of(u) / map(p.1of(p);v)]) ( < x,apply_alist([u / v];x;d) > [u / v])| 1 | 6. d: T 7. x: Label 8. x = 1of(u) (x map(p.1of(p);v)) < x,apply_alist([u / v];x;d) > = u ( < x,apply_alist([u / v];x;d) > v) |
About:
 |  |  |  |  |  |  |  |  |  |