'b,'a:S, l:'a List, f:('a'b). ||map(f;l)|| = ||l||  

By:	RewriteOfThm Thm* 'b,'a:S. Thm* all(l:hlist('a). all(f:'a  'b. equal(length(map(f,l)),length(l)))) (SimpsetC [`hol_to_nuprl`;`bequal`])

None

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