(13steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn is iseg
  T:Type, L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))
By: Unfold `iseg` 0 THEN ExRepD

Generated subgoals:

1 1. T : Type
2. L1 : T List
3. L2 : T List
4. l : T List
5. L2 = (L1 @ l)
  n:(||L2||+1). L1 = firstn(n;L2)
10 steps
2 1. T : Type
2. L1 : T List
3. L2 : T List
4. n : (||L2||+1)
5. L1 = firstn(n;L2)
  l:T List. L2 = (L1 @ l)
2 steps

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

(13steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc