Nuprl - Proof: choose elim neg 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: choose elim neg 1 2 1

1. 'a : S
2. P : 'a

Prop
3. Q : 'a

Prop
4.

x:'a. Q(x)

P(x)
5. (

x:'a.

Q(x))

(

x:'a. P(x))
6. {x:'a| Q(x) }

Void
7. x : 'a

Q(x)

By:	UnAb [`not`;`false`] THEN StrongAuto

Generated subgoal:

1 5. (x:'a. Q(x) Void) (x:'a. P(x))
6. {x:'a| Q(x) }Void
7. x : 'a
8. Q(x)
Void
2 steps

About:

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