Nuprl - Proof: choose elim pos 1

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

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

Prop
3. Q : 'a

Prop
4.

x:'a. Q(x)

P(x)
5.

x:'a. Q(x)

P(InjCase(lem({x:'a| Q(x) }); x. x, arb('a)))

By:	GenDC (lem({x:'a\| Q(x) })) THEN StrongAuto

Generated subgoals:

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

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

About:

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

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