(11steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list decomp reverse 1 1

1. T : Type
2. T List
  0<||nil||  (x:TL':T List. nil = (L' @ [x]))


By: Reduce 0


Generated subgoals:

None

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

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