Nuprl - Proof: choose true 1 2

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

1. 'a : Type
2. P : 'a

Prop
3. x : 'a
4. P(x)
5. {x:'a| P(x) }

Void

P(arb('a))

By:

Analyze 5

Generated subgoal:

1 {x:'a| P(x) }
1 step

About:

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