Nuprl - Proof: choose true 1 1

(5steps total) PrintForm hol Sections HOLlib Doc

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

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

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

P(x2)

By:	AddEMHyp THEN Analyze 5

Generated subgoals:

None

About:

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

(5steps total) PrintForm hol Sections HOLlib Doc