Nuprl - Proof: sum switch 1 2 2 1 2 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sum switch 1 2 2 1 2 2 1 1

1. n :

2. f :

3. i :

(n-1)
4. (i, i+1)

n
5. i1 :

(n-i-2)

f((i, i+1)(i1+2+i)) = f(i1+2+i)

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