IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable and
1
1. P : Prop
2. Q : Prop
3. P P
4. Q Q
P & Q (P & Q)
By: |
Analyze 4 THEN Analyze 3 |
Generated subgoals:
1 |
3. P
4. Q
P & Q (P & Q)
| 1 step |
2 |
3. P
4. Q
P & Q (P & Q)
| 1 step |
3 |
3. P
4. Q
P & Q (P & Q)
| 1 step |
4 |
3. P
4. Q
P & Q (P & Q)
| 1 step |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html