1. 
2. 
3. n : 
4. 0<n
  f:(). one_one(;;f) & onto(;;f)

By:	(DTerm (m:. m+1) 0) THEN (Unab [`one_one`;`onto`;`not`])

1	(m:. m+1)	1 step
2	(x,y:. (m:. m+1)(x) = (m:. m+1)(y)    x = y)   & ((y:. x:. y = (m:. m+1)(x)  )  False)	3 steps
3	5. f :    (one_one(;;f) & onto(;;f))  Prop	1 step

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