(5steps 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: member-es-interval 1 1 1
1. es : ES
2. e : E
3. e' : E
4. ev : E
5. e  ev 
6. ev  e' 
  (ev <loc e')  ev = e'  False
By: Unfold `es-le` -1 THEN ParallelOp -1

Generated subgoal:

1 6. ev = e'
  ev = e'  False
1 step

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

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