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

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

1

8. i<||a||   f(a[i]) = g(a[i])

1 step

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