Nuprl - Proof: honto def 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: honto def 1

1. 'a : S
2. 'b : S
3. f : 'a

(

onto('a;'b;f)) = (

y:'b. (

x:'a. (y =

(f(x)))))

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

Generated subgoals:

1 4. y:'b. x:'a. y = f(x)
5. y : 'b
x:'a. y = f(x)
1 step

2 4. y:'b. x:'a. y = f(x)
5. y : 'b
x:'a. y = f(x)
1 step

About:

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

1	4. y:'b. x:'a. y = f(x) 5. y : 'b x:'a. y = f(x)	1 step
2	4. y:'b. x:'a. y = f(x) 5. y : 'b x:'a. y = f(x)	1 step