Nuprl - Proof: num iso 2 1 1 1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 2 1 1 1 1 2 1

3. n :

4. 0<n
5. f :

6. one_one(

;

;f)
7.

onto(

;

;f)

x = f(y)

By:	Unab [`onto`] THEN Simpset [`not`] THEN Simp THEN StrongAuto

Generated subgoals:

None

About:

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