Nuprl - Proof: hsuc rep def 1 1

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

1. x :

(@f:

. (one_one(

;

;f) &

onto(

;

;f)))(x)

. ((

one_one(

;

;f))

(

onto(

;

;f))))(x)

By:	Unab [`bchoose`] THEN Simp THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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