(8steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn map
  f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))
By: InductionOnNat

Generated subgoals:

1 1. f : TopTop
  l:Top List. firstn(0;map(f;l)) ~ map(f;firstn(0;l))
1 step
2 1. f : TopTop
2. n : 
3. 0<n
4. l:Top List. firstn(n-1;map(f;l)) ~ map(f;firstn(n-1;l))
  l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))
6 steps

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

(8steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc