1. T : Type
2. L : T List
3. P : TT
  0sum(if (i<j)P(L[i],L[j]) 1 else 0 fi | i < ||L||; j < ||L||)

By:	Unfold `double_sum` 0 THEN BackThru Thm* n:, f:(n). (x:n. 0f(x))  0sum(f(x) | x < n) THEN BackThru Thm* n:, f:(n). (x:n. 0f(x))  0sum(f(x) | x < n)

1

4. i : ||L|| 5. j : ||L||   0if (i<j)P(L[i],L[j]) 1 else 0 fi

1 step

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