Nuprl - Proof: choose elim pos 1 2

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

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

Prop
3. Q : 'a

Prop
4.

x:'a. Q(x)

P(x)
5.

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

Void

P(arb('a))

By:	Analyze 5 THEN StrongAuto

Generated subgoal:

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

About:

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