IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
bij imp exists inv version21111 1. A : Type
2. B : Type
3. f : AB 4. Inj(A; B; f)
5. b : B 6. a : A 7. f(a) = b 8. a' : A 9. f(a') = b a' = a
By:
BackThru: Hyp:4
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
B
a' = a
