Nuprl - Proof: Dconstant realizes 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: Dconstant realizes 2

1. T : Type
2. c : T
3. x : Id
4. i : Id
5. (

loc.

(Dconstant(loc;T;c;x;i)))

Dsys
6. D' : Dsys
7.

loc.

(Dconstant(loc;T;c;x;i))

D'
8. w : World
9. p : FairFifo
10. PossibleWorld(D';w)

e@i.(x when e) = c

(x after e) = c

By:	Assert e@i.(x after e) = (x when e)

Generated subgoals:

1   e@i.(x after e) = (x when e)  T
1 step

2 11. e@i.(x after e) = (x when e)  T
  e@i.(x when e) = c  T  (x after e) = c  T
1 step

About:

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

1	e@i.(x after e) = (x when e) T	1 step
2	11. e@i.(x after e) = (x when e) T e@i.(x when e) = c T (x after e) = c T	1 step