T:Type, L_1,L_2:T List. L_1  L_2  L_1  L_2

By:	Unfold `sublist` 0 THEN Inst Thm* l1,l2:T List. l1  l2  ||l1||||l2|| [T;L_1;L_2] THEN Inst Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i]) [T;L_1;L_2] THEN InstConcl [i.i] THEN Reduce 0 THEN Try (BackThru Thm* k:. increasing(i.i;k))

1

1. T : Type 2. L_1 : T List 3. L_2 : T List 4. L_1  L_2 5. ||L_1||||L_2|| 6. L_1  L_2  ||L_1||||L_2|| & (i:. i<||L_1||  L_1[i] = L_2[i]) 7. L_1  L_2  (||L_1||||L_2|| & (i:. i<||L_1||  L_1[i] = L_2[i])) 8. j : ||L_1||   L_1[j] = L_2[j]

1 step

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