1. A : Type
2. F : AProp
3. A List
4. k:A. Dec(F(k))
5. u : A
6. v : A List
7. Dec((kv.F(k)))
  Dec((k[u / v].F(k)))

By:	RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x)  (yL.P(y)) 0

1

Dec(F(u)  (kv.F(k)))

1 step

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