Nuprl - Proof: change-lemma 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: change-lemma 1 2

1. es : ES
2. x : Id
3. i : Id
4. T : Type
5.

x,y:T. Dec(x = y)
6. vartype(i;x)

r T
7. e' : E
8. e : E
9.

e:E. loc(e) = i

(x when e)

T
10.

e:E. loc(e) = i

(x after e)

T
11. e

e'
12. loc(e') = i

loc(e) = i

By:	Unfold `es-le` -2 THEN Analyze -2

Generated subgoals:

1 11. (e <loc e')
12. loc(e') = i  Id
  loc(e) = i  Id
1 step

2 11. e = e'
12. loc(e') = i  Id
  loc(e) = i  Id
1 step

About:

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

1	11. (e <loc e') 12. loc(e') = i Id loc(e) = i Id	1 step
2	11. e = e' 12. loc(e') = i Id loc(e) = i Id	1 step