P:(L:(T List)
(||L||-1)
), m:((T List)).
Thm* (
L:T List, i:(||L||-1).
Thm* (P(L,i)
P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L))
Thm*
Thm* (
L:T List.
Thm* (
L':T List.
Thm* ((L guarded_permutation(T;
L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i)))f:(TT), m:(T).
Thm* (
x:T. m(f(x))
m(x) & (m(f(x)) = m(x) f(x) = x))
Thm*
Thm* (
x:T. n:. f(f^n(x)) = f^n(x))P:(L:(T List)(||L||-1)Prop).
Thm* Trans(T List)(_1 guarded_permutation(T;P) _2)
R:(TTProp), x,y:T. (x R y) (x (R^*) y)k:, P:(k).
Thm* ((
i:k. P(i)) 
0<search(k;P))
Thm* & (0<search(k;P)
P(search(k;P)-1) & (j:k. j<search(k;P)-1 P(j)))L:T List. L = nil 0<||L||L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| 
l:T List. ||l|| = 0 l = nilx,y:T, R:(TTProp). x = y (x (R^*) y)