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

1

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

9 steps

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