T:Type, as:(LabelT) List, d:T, x:Label. (x 1of(unzip(as))) ( < x,apply_alist(as;x;d) > as)

1	1. T: Type 2. as: (LabelT) List d:T, x:Label. (x nil) ( < x,apply_alist(nil;x;d) > nil)
2	1. T: Type 2. as: (LabelT) List 3. u: LabelT 4. v: (LabelT) List 5. 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])

About: