IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
choose elim neg111 1. 'a : S
2. P : 'aProp
3. Q : 'aProp
4. x:'a. Q(x) P(x)
5. (x:'a. Q(x)) (x:'a. P(x))
6. x : 'a 7. Q(x)
8. XM
P(x)
By:
BackThru 4 THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
x:'a. Q(x) 
P(x)
Q(x)) 
P(x)
