Nuprl - Proof: sublist tl

(4steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sublist tl

T:Type, L1,L2:T List.

null(L2)

tl(L2)

By:	InductionOnList

Generated subgoals:

1 1. T : Type
2. T List
3. L2 : T List
4. null(L2)
5. nil  tl(L2)
  nil  L2
1 step

2 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. L2 : T List
7. null(L2)
8. [u / v]  tl(L2)
  [u / v]  L2
2 steps

About:

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

(4steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc

1	1. T : Type 2. T List 3. L2 : T List 4. null(L2) 5. nil tl(L2) nil L2	1 step
2	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. L2 : T List 7. null(L2) 8. [u / v] tl(L2) [u / v] L2	2 steps