IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ooc preserves unb inf11 1. A : Type
2. B : Type
3. A ~ B 4. k : 5. (k injA)
(k injB)
By:
Rewrite by A ~ B
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(
A)
