IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hd l interval1 1. T : Type
2. l : T List
3. i : ||l||
4. j : i hd(l_interval(l;j;i)) ~ l_interval(l;j;i)[0]
By:
Unfold `select` 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
||l||
hd(l_interval(l;j;i)) ~ l_interval(l;j;i)[0]
