the_w:World, e:E. val(e)  V(loc(e);kind(e))

By:	Auto THEN Inst Thm* the_w:World, i:Id, a:Action(i). isnull(a)  val(a)  valtype(i;a) [the_w;loc(e);act(e)] THEN Try (BackThru Thm* the_w:World, e:E. isnull(act(e)))

1

1. the_w : World 2. e : E 3. val(act(e))  valtype(loc(e);act(e))   val(e)  V(loc(e);kind(e))

3 steps

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