Nuprl - Proof: rel exp list 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel exp list 1 1

1. T : Type
2. R : T

Prop
3. x : T
4. y : T
5. L : T List
6. ||L|| = 1
7. L[0] = x
8. L[(||L||-1)] = y
9.

0. L[i] R L[(i+1)]

x = y

By:	HypSubstSq -4 -2 THEN Reduce -2

Generated subgoals:

None

About:

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