IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sum switch1211 1. n : 2. f : n 3. i : (n-1)
4. (i, i+1) nn 5. i1 : i f((i, i+1)(i1)) = f(i1)
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
f((i, i+1)(i1)) = f(i1)
