Nuprl - Proof: not over exists 1

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

1. T : Type
2. Q : T

Prop
3.

(

x:T. Q(x))
4. x : T

Q(x)

By:	(Analyze 0) THEN (Analyze 3) THEN Witness x

Generated subgoals:

None

About:

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