Nuprl - Proof: exists over and r 1

(3steps total) PrintForm core StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exists over and r 1

1. T : Type
2. A : Prop
3. B : T

Prop
4. x : T
5. A
6. B(x)

x:T. B(x)

By:

Witness x

Generated subgoals:

None

About:

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

(3steps total) PrintForm core StandardLIB Doc