(2steps 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: es-before wf
  the_es:ES, e:E. before(e)  E List
By: StrongLocLessInd

Generated subgoal:

1 1. the_es : ES
2. e : E
3. x:E. (x <loc e)  before(x)  E List
  before(e)  E List
1 step

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

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