IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable vs unique nsub211221 1. P : Prop
2. P 3. i : 2
4. if i=0P else P fi
i = 1 2
By:
SplitITE Hyp:-1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
P
2
0
P else 
i = 1 
