Nuprl - Proof: member-es-interval 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: member-es-interval 1 1

1. es : ES
2. e : E
3. e' : E
4. ev : E

(ev <loc e')

ev = e'

False & e

ev & ev

By:	Auto THEN SplitOrHyps THEN Try (Unfold `es-le` 0 (THEN (((OrLeft THEN Complete Auto) ORELSE (OrRight THEN Complete Auto)))

Generated subgoal:

1 5. e  ev
6. ev  e'
  (ev <loc e')  ev = e'  False
2 steps

About:

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