1. A : Type
2. f : A
3. A List
4. u : A
5. 0<||nil||  (anil.(xnil.f(x)f(a)))
6. 0<||nil||+1
  (x[u].f(x)f(u))

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

None

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