Nuprl - Proof: iseg is sublist 1

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

1. T : Type
2. L_1 : T List
3. L_2 : T List
4. L_1

L_2
5. ||L_1||

||L_2||
6. L_1

L_2

||L_1||

||L_2|| & (

. i<||L_1||

L_1[i] = L_2[i])
7. L_1

L_2

(||L_1||

||L_2|| & (

. i<||L_1||

L_1[i] = L_2[i]))
8. j :

||L_1||

L_1[j] = L_2[j]

By:	ThinTrivial THEN ExRepD THEN EasyHyp

Generated subgoals:

None

About:

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