(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 1
1. T : Type
2. T List
3. l : T List
  nil = firstn(0;l)
By: Symmetry THEN BackThru Thm* l:T List. ||l|| = 0    l = nil

Generated subgoal:

1   ||firstn(0;l)|| = 0  
1 step

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