(6steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn all 1 1 1
1. Top List
2. u : Top
3. v : Top List
4. n:. ||v||n  (firstn(n;v) ~ v)
5. n : 
6. ||v||+1n
7. 0<n
  [u / firstn(n-1;v)] ~ [u / v]
By: Analyze THEN Try Trivial

Generated subgoal:

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

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

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