Nuprl - Proof: pair wd

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pair wd

'a,'b:S, x:('a

'b). <1of(x),2of(x)> = x

By:	RewriteOfThm Thm* 'a,'b:S. all(x:hprod('a; 'b). equal(pair(fst(x),snd(x)),x)) HNC

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html