IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose flips append12 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) @ map(i.(i, i+1);L2))
kk
By:
Fold `compose_flips` 0 THEN RWO "compose_append<" 0