1 |
1. T : Type
2. T' : Type
3. a : T List
4. x : T'
5. f : T T'
6. i: . i<||map(f;a)|| & x = map(f;a)[i]
y:T. ( i: . i<||a|| & y = a[i]) & x = f(y)
 | 3 steps |
2 |
1. T : Type
2. T' : Type
3. a : T List
4. x : T'
5. f : T T'
6. y:T. ( i: . i<||a|| & y = a[i]) & x = f(y)
i: . i<||map(f;a)|| & x = map(f;a)[i]
 | 3 steps |