1. T : Type
2. L1 : T List
3. L2 : T List
4. l : T List
5. L2 = (L1 @ l)
  n:(||L2||+1). L1 = firstn(n;L2)

By:	((HypSubst -1 0) (THEN ((RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   0)) THEN InstConcl [||L1||]

1

L1 = firstn(||L1||;L1 @ l)

9 steps

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