IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iseg member11 1. T : Type
2. l1 : T List
3. l2 : T List
4. x : T 5. ||l1||||l2||
6. i:. i<||l1|| l1[i] = l2[i]
7. i : 8. i<||l1||
9. x = l1[i]
x = l2[i]
By:
WeakSubstFor x 0 THEN Easy
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
||l2||
i:
. i<||l1|| 
l1[i] = l2[i]
x = l2[i]
