Def es-ble{i:l}(es;e;e')
Def == InjCase(decidable__es_DASH_le{1:l, i:l}(es,e',e); x. true, false)

is mentioned by

Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e')  e  e'	[assert-es-ble]
Def [e, e'] == filter(ev.es-ble{i:l}(es;e;ev);before(e') @ [e'])	[es-interval]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html