IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem | Name |
Thm* (A bij B) (A inj B) | [bijection_type_inc_inj] |
cites the following: |
Thm* (A bij B) (A inj B) | [bijtype_sub_injtype] |
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html