Nuprl - Proof: permute by flips 2 2 1 2 1 1 1 1 1 1 1 1 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 1

1. k :

(k-1-1) List
3. 0<k

compose_flips(nil)(k-1) = k-1

By:	Unfold `compose_flips` 0 THEN Reduce 0

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html