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||
  f:((T List)(T List)). 
  L:T List. 
  f(L)
  =
  if null(L) L
  else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi

By:	InstConcl [L.if null(L) L [L.else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi]

1	(L.if null(L) L   (L.else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi)    (T List)(T List)	1 step
2	L:T List.    (L.if null(L) L   (L.else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi)   (L)   =   if null(L) L   else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi	1 step
3	7. f : (T List)(T List)   (L:T List.    (f(L)   (=   (if null(L) L   (else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi)    Prop	1 step

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