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

By:	InstHyp [i+1;j+1] -3 THEN RWO Thm* x:T, l:T List, i:||l||. [x / l][(i+1)] ~ l[i] -1

None

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