Nuprl - Proof: exists functionality wrt iff 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exists functionality wrt iff 1

1. S : Type
2. T : Type
3. P : S

Prop
4. Q : S

Prop
5. S = T
6.

x:S. P(x)

Q(x)
7.

x:S. P(x)

y:T. Q(y)

By:	(Analyze 7 THEN Witness x) THEN HypBackchain

Generated subgoals:

None

About:

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