7. d2: T
8. x: Label
9. (x
1of(unzip([u / v])))10.
1of(u) =
x
apply_alist(v;x;d1) = apply_alist(v;x;d2)
T) ListTT) List
d1,d2:T, x:Label. (x 1of(unzip(v))) 
apply_alist(v;x;d1) = apply_alist(v;x;d2) d1,d2:T, x:Label.
(x 1of(unzip([u / v]))) apply_alist([u / v];x;d1) = apply_alist([u / v];x;d2)as:(LabelT) List, p:(LabelT), l:Label, d:T.
apply_alist([p / as];l;d) ~ if 1of(p) = l
2of(p) else apply_alist(as;l;d) fi
[T;v;u;x;d1]
as:(LabelT) List, p:(LabelT), l:Label, d:T.
apply_alist([p / as];l;d) ~ if 1of(p) = l 2of(p) else apply_alist(as;l;d) fi
[T;v;u;x;d2]
| 1 | 6. d1: T 7. d2: T 8. x: Label 9. (x 1of(unzip([u / v])))10. 1of(u) = x apply_alist(v;x;d1) = apply_alist(v;x;d2) |
About:
 |  |  |  |  |  |  |