(2steps 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: 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:i<||L_1||  L_1[i] = L_2[i])
7. L_1  L_2  (||L_1||||L_2|| & (i: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:
listnatural_numberless_thanuniverseequalimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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