(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 1 1
1. T : Type
2. L1 : T List
3. L2 : T List
4. l : T List
5. L2 = (L1 @ l)
  L1 = firstn(||L1||;L1 @ l)
By: ThinVar `L2'

Generated subgoal:

1 3. l : T List
  L1 = firstn(||L1||;L1 @ l)
8 steps

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