Nuprl - Proof: ax choice version3 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ax choice version3 2 1

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

Prop
4. f : A

B
5.

x:A. Q(x,f(x))
6. x : A

y:B. Q(x,y)

By:	Witness: f(x) THEN BackThru: Hyp:5

Generated subgoals:

None

About:

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