Nuprl - Proof: change-lemma 1 1 2 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: change-lemma 1 1 2 2 1 1 1 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. loc(e) = i

(x when e)

T
8.

e:E. loc(e) = i

(x after e)

T
9. WellFnd{i}(E;x,y.(x <loc y))
10. j : E
11.

k:E.
11. (k <loc j)
11.

11. (

e:E.
11. (e

k
11. (

11. (loc(k) = i
11. (

11. (

(

[e, k].

(x after ev) = (x when ev))

(x after k) = (x when e))
12. e : E
13. e

j
14. loc(j) = i
15.

(

[e, j].

(x after ev) = (x when ev))

(x after j) = (x when e)

By:	Decide ((x after j) = (x when j)) THENA BackThruSomeHyp

Generated subgoals:

1 16. (x after j) = (x when j)  T
  (x after j) = (x when e)  T
38 steps

2 16. (x after j) = (x when j)  T
  (x after j) = (x when e)  T
3 steps

About:

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

1	16. (x after j) = (x when j) T (x after j) = (x when e) T	38 steps
2	16. (x after j) = (x when j) T (x after j) = (x when e) T	3 steps