Nuprl - Proof: decidable equal int seg

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable equal int seg

i,j:

, x,y:{i..j

}. Dec(x = y)

By:	Unfold `decidable` 0 THEN RepD

Generated subgoal:

1 1. i :
2. j :
3. x : {i..j}
4. y : {i..j}
x = y x = y
4 steps

About:

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