IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iseg is sublist1 1. T : Type
2. L_1 : T List
3. L_2 : T List
4. L_1L_2 5. ||L_1||||L_2||
6. L_1L_2 ||L_1||||L_2|| & (i:. i<||L_1|| L_1[i] = L_2[i])
7. L_1L_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:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html