Nuprl - Proof: es-ble wf 1 1

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

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

e',e:E

Dec(e

e' )
5. v1 : Dec(e

e' )

InjCase(v1; x. true

, false

)

By:	Analyze -1 THEN Reduce 0

Generated subgoals:

None

About:

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