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:	Inst Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||   [T;T';f;a] THEN Inst Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||   [T;T';g;a]

None

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