Nuprl - Proof: member iff sublist 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: member iff sublist 1 2

1. T : Type
2. x : T
3. L : T List
4. i :

5. i<||L||
6. x = L[i]
7. j :

[x][j] = L[((

x.i)(j))]

By:	AssertBY (j = 0) Auto THEN HypSubstSq -1 0 THEN Reduce 0

Generated subgoals:

None

About:

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