L:T List, P:(T
TProp).
Thm* (
x,y:T. Dec(P(x,y)))
Thm*
Thm* (
x,y:T. 
P(x,y) P(y,x))
Thm*
Thm* (
L':T List.
Thm* ((L (swap adjacent[
P(x,y)]^*) L') & (i:
(||L'||-1). P(L'[i],L'[(i+1)])))L:T List, P:(TT
).
Thm* (
x,y:T. P(x,y) P(y,x))
Thm*
Thm* (
L':T List.
Thm* ((L guarded_permutation(T;
L,i. P(L[i],L[(i+1)])) L')
Thm* (& (
i:(||L'||-1). P(L'[i],L'[(i+1)])))R1,R2:(TTProp), x,y:T. R1 => R2 (x (R1^*) y) (x (R2^*) y)