T:Type, as,bs:T List, i:{||as||..(||as||+||bs||)}.
  (as @ bs)[i] = bs[(i-||as||)]

1

1. T : Type 2. as : T List 3. bs : T List 4. i : {||as||..(||as||+||bs||)}   (as @ bs)[i] = bs[(i-||as||)]

5 steps

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