T:Type, as:T List, x:T. 0<||as||  (x  tl(as))  (x  as)

1

1. T : Type 2. as : T List 3. x : T 4. 0<||as|| 5. i :  6. i<||tl(as)|| 7. x = tl(as)[i]   i:. i<||as|| & x = as[i]

1 step

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