1. T : Type
2. P : L:(T List)(||L||-1)
3. m : (T List)
4. L:T List, i:(||L||-1).
4. P(L,i)  P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L)
5. L : T List
6. 0<||L||
  L guarded_permutation(T;L,i. P(L,i)) nil

By:	Unfold `guarded_permutation` 0 THEN Reduce 0 THEN BackThru Thm* x,y:T, R:(TTProp). x = y  (x (R^*) y) THEN BackThru Thm* l:T List. ||l|| = 0    l = nil

None

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