Nuprl - Proof: partition type 1

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

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

Prop
4.

x:A.

!y:B. P(x;y)

A ~ (y:B

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

By:	FwdThru: Thm* (x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x))) on [ Hyp:-1 ] THEN Analyze-1

Generated subgoal:

1 5. f : AB
6. x:A. P(x;f(x))
A ~ (y:B{x:A| P(x;y) })
12 steps

About:

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