IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l tricotomy111 1. T : Type
2. x : T 3. y : T 4. L : T List
5. i1 : 6. i1<||L||
7. x = L[i1]
8. i : 9. i<||L||
10. y = L[i]
11. i1<i 12. j : 2
13. j = 0
[x; y][j] = L[i1]
By:
HypSubstSq -1 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
[x; y][j] = L[i1]
