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
9. j = 0
  P([x / L][j],L[(i-1)])

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

1

P(L[(j-1)],L[(i-1)])

1 step

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