Nuprl Basics - Proof: sfa doc exteq gprop 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc exteq gprop 1 2

1. A : Type
2. P : A

Prop
3. f : x:A

Prop(given P(x))
4. x : {x:A| P(x) }

f(x)

Prop

By:

Analyze-1

Generated subgoal:

1 4. x : A
5. P(x)
f(x) Prop
2 steps

About:

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