Nuprl - Proof: Dconstant realizes 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: Dconstant realizes 2 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)
11.

e@i.(x after e) = (x when e)

e@i.(x when e) = c

(x after e) = c

By:	RepeatFor 3 (ParallelOp -1) THEN HypSubst -1 0

Generated subgoals:

None

About:

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