Nuprl - Proof: partition type 1 1

(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

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

1. A : Type
2. B : Type
3. P : A

Prop
4.

x:A.

!y:B. P(x;y)
5. f : A

B
6.

x:A. P(x;f(x))

A ~ (y:B

{x:A| P(x;y) })

By:	Witness: x.<f(x),x> \| yx.2of(yx)

Generated subgoals:

1 7. x : A
  x  {x@0:A| P(x@0;f(x)) }
1 step

2   InvFuns(A;y:B{x:A| P(x;y) };x.<f(x),x>;yx.2of(yx))
9 steps

3 7. (y:B{x:A| P(x;y) })A
8. x : A
  x  {x@0:A| P(x@0;f(x)) }
1 step

About:

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

(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

1	7. x : A x {x@0:A\| P(x@0;f(x)) }	1 step
2	InvFuns(A;y:B{x:A\| P(x;y) };x.<f(x),x>;yx.2of(yx))	9 steps
3	7. (y:B{x:A\| P(x;y) })A 8. x : A x {x@0:A\| P(x@0;f(x)) }	1 step