IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card nsub0 union 2
1
1. A : Type
(
0+A) ~ A
| By: |
BackThru: Thm* (0+A) ~ A |
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
