Nuprl - Proof: honto def 1 1

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

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

'b
4.

y:'b.

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

x:'a. y = f(x)

By:	BackThru 4 THEN Simp THEN StrongAuto

Generated subgoals:

None

About:

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