1. T : Type
2. x : T
3. L : T List
4. P : TTProp
5. i:||L||, j:i. P(L[j],L[i])
6. (yL.P(x,y))
7. i : ||[x / L]||
8. j : i
  P([x / L][j],[x / L][i])

By:	CaseNat 0 `j' THEN Reduce 0 THEN Subst (i ~ (i-1+1)) 0 THENL [Assert (i  );Id] THEN RWO Thm* x:T, l:T List, i:||l||. [x / l][(i+1)] ~ l[i] 0

1	9. j = 0   P(x,L[(i-1)])	2 steps
2	9. j = 0   P([x / L][j],L[(i-1)])	2 steps

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