Nuprl - Proof: l tricotomy 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: l tricotomy 1

1. T : Type
2. x : T
3. y : T
4. L : T List
5. i1 :

6. i1<||L||
7. x = L[i1]
8. i :

9. i<||L||
10. y = L[i]

x = y

[x; y]

[y; x]

By:	Tricotomy i1 i THENL [(Sel 1 (Analyze 0)) THEN (Sel 2 (Analyze 0)) ;(Sel 1 (Analyze 0)) THEN (Sel 1 (Analyze 0)) ;Sel 2 (Analyze 0)]

Generated subgoals:

1 11. i1<i
  [x; y]  L
3 steps

2 11. i1 = i
  x = y
1 step

3 11. i<i1
  [y; x]  L
5 steps

About:

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