IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length zero1 1. T : Type
2. u : T 3. v : T List
4. [u / v] = nil
||v||+1 = 0
By:
Obvious
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html