IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
bijection restriction111 1. k : 2. f : kk 3. 0<k 4. Bij(k; k; f)
5. f(k-1) = k-1
6. z : (k-1)
7. f(z) = k-1
f(z) (k-1)
By:
AllHyps (h.Unfold `biject` h THEN Unfold `inject` h THEN InstHyp [z;k-1] h)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
f(z) 
h.Unfold `biject` h THEN Unfold `inject` h THEN InstHyp [z;k-1] h)
