Nuprl - Proof: firstn map 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn map 2 2

1. f : Top

Top
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))

firstn(n;[(f(u)) / map(f;v)]) ~ map(f;firstn(n;[u / v]))

By:	RecUnfold `firstn` 0 THEN Reduce 0 THEN SplitOnConclITE

Generated subgoals:

1 9. 0<n
[(f(u)) / firstn(n-1;map(f;v))] ~ map(f;[u / firstn(n-1;v)])
2 steps

2 9. n0
nil ~ map(f;nil)
Auto

About:

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

1	9. 0<n [(f(u)) / firstn(n-1;map(f;v))] ~ map(f;[u / firstn(n-1;v)])	2 steps
2	9. n0 nil ~ map(f;nil)	Auto