IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
list decomp
1
1. T : Type
2. L : T List
3. 0<||L||
L ~ [hd(L) / tl(L)]
| By: |
ListInd 2 THEN Reduce 0 |
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
