IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
unb inf not fin
1
1
1. A : Type
2. Unbounded(A)
3. n :
4. A ~ n
False
Generated subgoal:
1 |
5. ((n+1) inj A)
False
| 2 steps |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html