At: apply alist property 1 1 2 2
1. T: Type
2. as: (Label
T) List
3. d: T
4. x: Label
5. i: 
6. i < ||as||
7. (first a 
as s.t. 1of(a) =
x else < x,d > ) = as[i]
8. z: LabelT
i < ||map(
p.2of(p);as)||
By: RWO "map_length" 0
Generated subgoals:None
About:
