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

By:	Auto THEN BackThru Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b

1

1. T : Type 2. L1 : T List 3. L2 : T List 4. L1  L2 5. ||L1|| = ||L2||   6. i :  7. i<||L1||   L1[i] = L2[i]

3 steps

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