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