IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose append2 1. T : Type
2. (TT) List
3. u : TT 4. v : (TT) List
5. L2:(TT) List. compose_list(v) o compose_list(L2) = compose_list(v @ L2)
6. L2 : (TT) List
u o compose_list(v) o compose_list(L2) = u o compose_list(v @ L2)