IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose flips append1 1. k : 2. L1 : (k-1) List
3. L2 : (k-1) List
compose_list(map(i.(i, i+1);L1)) o compose_list(map(i.(i, i+1);L2))
=
compose_list(map(i.(i, i+1);L1 @ L2))
kk