(27steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swap adjacent decomp 1 1 2
1. A : Type
2. L : A List
3. 1<||L||
4. ||tl(tl(L))|| = ||L||-2
  i:. i<||L||  L[i] = [L[0]; L[1] / tl(tl(L))][i]
By: Auto THEN CaseNat 0 `i' THEN Reduce 0

Generated subgoal:

1 5. i : 
6. i<||L||
7. i = 0
  L[i] = [L[0]; L[1] / tl(tl(L))][i]
6 steps

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

(27steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc