Nuprl - Proof: w-eval wf 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-eval wf 1 1

1. the_w : World
2. e : E
3. val(act(e))

valtype(loc(e);act(e))

V(loc(e);kind(e)) ~ valtype(loc(e);act(e))

By:	Repeat (Unfolds [`w-V`;`w-M`;`w-TA`;`w-valtype`;`w-ekind`] 0) THEN Trivial

Generated subgoals:

None

About:

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