Nuprl - Proof: hsuc rep def 1

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

(

. (@f:

. (one_one(

;

;f) &

onto(

;

;f)))(x))

. ((

one_one(

;

;f))

(

onto(

;

;f))))

By:	(Ext THEN HN) THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 1. x :
  (@f:. (one_one(;;f) & onto(;;f)))(x)
  =
  (@f:. ((one_one(;;f))(onto(;;f))))(x)
1 step

About:

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