(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 2
1. T : Type
2. T List
3. u : T
4. v : T List
5. 0<||v||  (x:T, L':T List. v = (L' @ [x]))
  0<||[u / v]||  (x:T, L':T List. [u / v] = (L' @ [x]))
By: Decide (||v||=0) THEN RW assert_pushdownC -1

Generated subgoals:

1 6. ||v|| = 0  
  0<||[u / v]||  (x:T, L':T List. [u / v] = (L' @ [x]))
4 steps
2 6. ||v||  0  
  0<||[u / v]||  (x:T, L':T List. [u / v] = (L' @ [x]))
3 steps

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