1. T : Type
2. T List
3. u : T
4. v : T List
5. P:(T). (xv.P(x))  reduce(x,y. P(x)y;true;v)
  P:(T). (x[u / v].P(x))  (P(u)reduce(x,y. P(x)y;true;v))

By:	RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) 0 THEN All (RW assert_pushdownC) THEN Easy

None

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