1. T : Type
2. P : TProp
3. x : T
4. L : T List
5. P(x)
6. y:T. (y  L)  P(y)
7. y : T
8. (y  [x / L])
  P(y)

By:	RWO Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l) -1 THEN Analyze -1

1	8. y = x   P(y)	1 step
2	8. (y  L)   P(y)	1 step

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