Nuprl - Proof: swap adjacent decomp 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swap adjacent decomp 1 1 1

1. A : Type
2. L : A List
3. 1<||L||
4. ||tl(tl(L))|| = ||L||-2

||L|| = ||[L[0]; L[1] / tl(tl(L))]||

By:

Reduce 0

Generated subgoals:

None

About:

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