Nuprl - Proof: reject cons hd

(3steps total) PrintForm Definitions list 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: reject cons hd

T:Type, a:T, as:T List, i:

. i

(a.as)\[i] = as

By:	UnivCD THEN RecUnfold `reject` 0 THEN SplitOnConclITE

Generated subgoals:

1 1. T : Type
2. a : T
3. as : T List
4. i :
5. i0
6. i0
tl((a.as)) = as
1 step

2 1. T : Type
2. a : T
3. as : T List
4. i :
5. i0
6. 0<i
(Case of a.as; nil nil ; a'.as' a'.as'\[i-1]) = as
1 step

About:

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

(3steps total) PrintForm Definitions list 1 Sections StandardLIB Doc

1	1. T : Type 2. a : T 3. as : T List 4. i : 5. i0 6. i0 tl((a.as)) = as	1 step
2	1. T : Type 2. a : T 3. as : T List 4. i : 5. i0 6. 0<i (Case of a.as; nil nil ; a'.as' a'.as'\[i-1]) = as	1 step