Nuprl - Proof: assert-w-eq-E 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert-w-eq-E 1

1. the_w : World
2. e : {p:(Id

isnull(a(1of(p);2of(p))) }
3. e' : {p:(Id

isnull(a(1of(p);2of(p))) }
4. 1of(e) = 1of(e')
5. 2of(e) = 2of(e')

e = e'

By:	DVar `e' THEN DVar `e\'' THEN Analyze THEN DVar `e' THEN DVar `e\'' THEN All Reduce THEN Analyze

Generated subgoals:

None

About:

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