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])
  map(f;a) = map(g;a)

By:	BackThru Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b

1	||map(f;a)|| = ||map(g;a)||	1 step
2	i:. i<||map(f;a)||  map(f;a)[i] = map(g;a)[i]	3 steps

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