IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable cand1122 1. P : Prop
2. Q : Prop given P 3. P 4. P Dec(Q)
5. (P & Q) Prop
P & Q(P & Q)
By:
OrRight THEN Analyze 0 THEN ExRepD
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html