T:Type, Q:((T List)Prop).
  Q(nil)
  
  (x:T. Q([x]))
  
  (ys,ys':T List. Q(ys)  Q(ys')  Q(ys @ ys'))  (zs:T List. Q(zs))

1

1. T : Type 2. Q : (T List)Prop 3. Q(nil) 4. x:T. Q([x]) 5. ys,ys':T List. Q(ys)  Q(ys')  Q(ys @ ys') 6. zs : T List   Q(zs)

3 steps

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