IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l before transitivity1 1. T : Type
2. l : T List
3. x : T 4. y : T 5. z : T 6. no_repeats(T;l)
7. [x; y] l 8. [y; z] l [x; z] l
By:
Using [`L2',[x; y; z]]
(BackThru Thm*L1,L2,L3:T List. L1L2L2L3L1L3)