PrintForm Definitions mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: length-map

  f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L||

By: InductionOnList THEN Reduce 0 THEN Analyze THEN Trivial


Generated subgoals:

None

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

PrintForm Definitions mb event system 1 Sections EventSystems Doc