Nuprl - Proof: reject cons tl 1

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

1. T : Type
2. a : T
3. as : T List
4. i :

5. 0<i
6. i

||as||

(a.as)\[i] = a.as\[i-1]

By:	RWN 1 (RecUnfoldTopC `reject`) 0 THEN SplitOnConclITE

Generated subgoals:

1 7. i0
tl((a.as)) = a.as\[i-1]
1 step

2 7. 0<i
(Case of a.as; nil nil ; a'.as' a'.as'\[i-1]) = a.as\[i-1]
2 steps

About:

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

1	7. i0 tl((a.as)) = a.as\[i-1]	1 step
2	7. 0<i (Case of a.as; nil nil ; a'.as' a'.as'\[i-1]) = a.as\[i-1]	2 steps