d1,d2:T, x:Label. (x 
map(
p.1of(p);v)) 
apply_alist(v;x;d1) = apply_alist(v;x;d2)6. d1: T
7. d2: T
8. x: Label
9. x = 1of(u)
10.
1of(u) =
x
(x map(p.1of(p);v))
T) ListTT) Listd1,d2:T, x:Label. (x 1of(unzip(v))) apply_alist(v;x;d1) = apply_alist(v;x;d2) 1of(unzip([u / v])))1of(u) = x apply_alist(v;x;d1) = apply_alist(v;x;d2)| 1 | 5. d1,d2:T, x:Label. (x map(p.1of(p);v)) apply_alist(v;x;d1) = apply_alist(v;x;d2) 6. d1: T 7. d2: T 8. x: Label 9. x = 1of(u) 10. 1of(u) = x (x map(p.1of(p);v)) |
About:
 |  |  |  |  |  |  |  |  |