IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
swap cons2111 1. T : Type
2. L : T List
3. x : T 4. i : {1..(||L||+1)}
5. j : {1..(||L||+1)}
6. i1 : 7. i1<||swap([x / L];i;j)||
8. i1 = 0
0<||[x / L]||
By:
Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
0<||[x / L]||
