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

By:	ExRepD THEN RWW Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||   -2 THEN RWW Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]) -1

1

6. i :  7. i<||a|| 8. x = f(a[i])   y:T. (i:. i<||a|| & y = a[i]) & x = f(y)

2 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html