1. A : Type
2. B : Type
3. f : AB
4. A List
5. u : A
6. v : A List
7. n:||v||. map(f;v)[n] = f(v[n])
8. n : (||v||+1)
9. n = 0
  (f(u).map(f;v))[n] = f((u.v)[n])

By:	RWH (LemmaC Thm* a:T, as:T List, i:. i0  (a.as)[i] = a) 0

None

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