Nuprl - Proof: Dconstant realizes 1

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

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)

(vartype(i;x)

r T) &

e@i.first(e)

(x when e) = c

By:

InitRule

Generated subgoals:

None

About:

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