Nuprl - Proof: least exists2 1 1 2 1 1 1

(9steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

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

1. P :

Prop
2.

i:

. P(i)
3. p :

4.

i:

. p(i)

P(i)
5. (least i:

. p(i))

{i:

| p(i) & (

j:

. j<i

p(j)) }
6. u :

7. p(u) & (

j:

. j<u

p(j))

P(u) & (

j:

. j<u

P(j))

By:	Rewrite by Hyp:4

Generated subgoals:

None

About:

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

(9steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc