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])
  (yL.P(x,y))

1

(yL.P(x,y))

3 steps

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