Nuprl - Proof: nsub inj ooc nsub bij

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

. (

k inj

k) ~ (

k bij

By:	Auto THEN OOCifExteq THEN BackThru: Thm* (k inj k) =ext (k bij k)

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