1. T : Type
2. T List
3. u : T
4. v : T List
5. L2:T List. null(L2)  v  tl(L2)  v  L2
6. T List
7. u1 : T
8. v1 : T List
9. null(v1)  [u / v]  tl(v1)  [u / v]  v1
10. False
11. [u / v]  v1
  [u / v]  [u1 / v1]

By:	RWO Thm* x1,x2:T, L1,L2:T List. Thm* [x1 / L1]  [x2 / L2]  x1 = x2 & L1  L2  [x1 / L1]  L2 0 THEN OrRight

None

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