T:Type, a,b:T List.
  ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b

1

1. T : Type 2. a : T List 3. b : T List 4. ||a|| = ||b||   5. i:. i<||a||  a[i] = b[i]   a = b

6 steps

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