T:Type, L:T List. L  nil  L = nil

By:	Auto THEN Try (BackThru Thm* l:T List. ||l|| = 0    l = nil (THEN (FwdThru Thm* L1,L2:T List. L1  L2  ||L1||||L2|| [-1] (THEN (Reduce -1)

1

1. T : Type 2. L : T List 3. L = nil   L  nil

1 step

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