Nuprl - Proof: swap length 1

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

1. T : Type
2. L : T List
3. i :

||L||
4. j :

||L||

||swap(L;i;j)|| = ||L||

By:	Unfold `swap` 0 THEN BackThru Thm* L:T List, f:(\|\|L\|\|\|\|L\|\|). \|\|(L o f)\|\| = \|\|L\|\|

Generated subgoals:

None

About:

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