U
f(x) = (
x.x/l,r. f( < l,r > ))(x) TU = TU f = f (x.x/l,r. f( < l,r > )) = (x.x/l,r. f( < l,r > )) 
TU
VUV
f = (x.x/l,r. f( < l,r > ))
| 1 | 5. x: TU f(x) = (x.x/l,r. f( < l,r > ))(x) |
| 2 | TU = TU |
| 3 | f = f |
| 4 | (x.x/l,r. f( < l,r > )) = (x.x/l,r. f( < l,r > )) TUV |
About:
 |  |  |  |  |  |  |  |