Nuprl - Proof: hsuc rep def

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

equal(suc_rep,select(

f:hind

hind. and(one_one(f),not(onto(f)))))

By:	HN THEN StrongAuto THEN Unab [`hsuc_rep`] THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

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

About:

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