T:Type, L1,L2:T List. L1 = L2  L1  L2

By:	Unfold `sublist` 0 THEN InstConcl [i.i] THEN Reduce 0 THEN Try (Complete (WeakSubstFor L2 0)) THEN Try Analyze THEN Try Auto

1

1. T : Type 2. L1 : T List 3. L2 : T List 4. L1 = L2   increasing(i.i;||L1||)

1 step

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