(2steps total) PrintForm Definitions LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: disjunct elim
  P,Q:Prop. P  Q  P  Q
By: Auto

Generated subgoal:

1 1. P : Prop
2. Q : Prop
3. P  Q
4. P
  Q
1 step

About:
propimpliesorall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(2steps total) PrintForm Definitions LogicSupplement Sections DiscrMathExt Doc