T:Type, L1,L2:T List. L1  L2  L2  L1  L1 = L2

By:	Auto THEN BackThru Thm* L1,L2:T List. L1  L2  ||L1|| = ||L2||    L1 = L2

1

1. T : Type 2. L1 : T List 3. L2 : T List 4. L1  L2 5. L2  L1   ||L1|| = ||L2||

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html