IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable vs unique nsub2
1
2
1
2
1. P : Prop
2. i :
2
3.
P
4. i
0
Dec(P)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html