Nuprl - Proof: permute by flips 2 2 1 2 1 1 1 1 1 1 1 1 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: permute by flips 2 2 1 2 1 1 1 1 1 1 1 1 1 2 1 1

1. k :

(k-1-1) List
3. 0<k
4. u :

(k-1-1)
5. v :

(k-1-1) List
6. compose_flips(v)(k-1) = k-1
7. 0

compose_flips(v)(k-1) < k

(u, u+1)(k-1) = k-1

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