Alph*Prop
x:Alph*. R(x,x)x,y:Alph*. R(x,y) 
R(y,x)x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)x,y,z:Alph*. R(x,y) R((z @ x),z @ y)nAlph*l:Alph*. 
i:n. R(l,w(i))
n
nnx:Alph*. R(x,w(f(x)))n
n(nn)nn; (nn); f1)
a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c)n:{1...}, m:{n+1...}, f:(mn). i,j:m. i < j & f(i) = f(j)
[nn;nn+1;
j.f1( < f((a[||a||-j..||a||
]) @ b),f((a[||a||-j..||a||]) @ c) > )]| 1 | 1 nn |
| 2 | 18. i,j:(nn+1).
i < j
& (j.f1( < f((a[||a||-j..||a||]) @ b),f((a[||a||-j..||a||]) @ c) > ))(i)
=
(j.f1( < f((a[||a||-j..||a||]) @ b),f((a[||a||-j..||a||]) @ c) > ))(j)
 (nn) a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |