(12steps 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: nth tl decomp 1
1. T : Type
2. L : T List
3. 0<||L||
4. 00
  L ~ [hd(L) / tl(L)]
By: BackThru Thm* L:T List. 0<||L||  (L ~ [hd(L) / tl(L)])

Generated subgoals:

None

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

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