1. w : World
2. FairFifo
  e:E. 
  V(loc(e);kind(e)) = eventtype(e.kind(e);e.loc(e);i,a. V(i;locl(a));w.M;e)

By:	Auto THEN Subst (eventtype(e.kind(e);e.loc(e);i,a. V(i;locl(a));w.M;e) ~ V(loc(e);kind(e))) 0 THENL [Unfolds [`w-V`;`w-M`;`eventtype`] 0 THEN Reduce 0 THEN Trivial;Auto]

None

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