(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 2 2 1

1. f : TopTop
2. n : 
3. 0<n
4. l:Top List. firstn(n-1;map(f;l)) ~ map(f;firstn(n-1;l))
5. Top List
6. u : Top
7. v : Top List
8. firstn(n;map(f;v)) ~ map(f;firstn(n;v))
9. 0<n
  [(f(u)) / firstn(n-1;map(f;v))] ~ map(f;[u / firstn(n-1;v)])


By: Reduce 0 THEN Analyze THEN Try Trivial


Generated subgoal:

1   firstn(n-1;map(f;v)) ~ map(f;firstn(n-1;v))
1 step

About:
listconsintnatural_numbersubtractless_thanapplyfunctionsqequaltopall
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