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