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