Nuprl - Proof: change-lemma 1 2 1

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

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 <loc e')
12. loc(e') = i

loc(e) = i

By:	Unfold `es-locl` -2

Generated subgoals:

None

About:

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