Nuprl - Proof: exteq sigma st dom 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exteq sigma st dom 1 2 1

1. A : Type
2. B : A

Type
3. P : A

Prop
4. i : A
5. b : B(i)
6. P(i)

<i,b>

i:{i:A| P(i) }

B(i)

By:

Analyze

Generated subgoals:

1 i {i:A| P(i) }
Auto

2 b B(i)
Trivial

About:

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