n15.
x:Alph*. R(x,w(f(x)))
a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c)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
n a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c)Q:(ABProp). (x:A. y:B. Q(x,y)) (f:(AB). x:A. Q(x,f(x)))
[Alph*;n;
l,i. R(l,w(i))]
| 1 | 14. f: Alph*n 15. x:Alph*. R(x,w(f(x))) a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |