Nuprl - mb_list_1 LEMMAs for map

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

Rank	Theorem	Name
2	Thm* a:T List, f,g:(TT'). Thm* (i:. i<\|\|a\|\| f(a[i]) = g(a[i])) map(f;a) = map(g;a)	[map_equal]
cites the following:
1	Thm* a,b:T List. \|\|a\|\| = \|\|b\|\| (i:. i<\|\|a\|\| a[i] = b[i]) a = b	[list_extensionality]
1	Thm* f:(AB), as:A List, n:\|\|as\|\|. map(f;as)[n] = f(as[n])	[map_select]
0	Thm* f:(AB), as:A List. \|\|map(f;as)\|\| = \|\|as\|\|	[map_length]

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