(4steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-eval wf 1
1. the_w : World
2. e : E
3. val(act(e))  valtype(loc(e);act(e))
  val(e)  V(loc(e);kind(e))
By: NthHypSq -1 THEN Analyze

Generated subgoals:

1   V(loc(e);kind(e)) ~ valtype(loc(e);act(e))
1 step
2   val(e) ~ val(act(e))
1 step

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

(4steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc